Re: [isabelle] Isabelle2021-1-RC3 available for testing

On 2021-11-14 21:48, Peter Lammich wrote:
Hi List.

Following my experience report on porting isabelle-llvm from 2021 to
Summary: roughly 7h work for 70kLOC.
Fixing violations of context discipline took a while, and bigger
changes in word library (again) were getting a little annoying.
Otherwise, everything worked well.

Apart from the separate emails I already sent, one minor point I
noticed: substitutions work with a more efficient data structure now.
However, the existing NEWS entry does not mention Variable.import,
where this change caused type errors for me at several points.
Thus, I needed some time to find the relevant NEWS entry.


On Fri, 2021-11-12 at 21:26 +0100, Makarius wrote:
Dear Isabelle users,

please see and
for further progress on the release process.

There is now a proper download for Linux (ARM), and the "isabelle
build_docker" tools works for it (relevant on Apple M1 hardware).

This is also the fork-point of the isabelle-dev repository, which
for the time after this release:

Reminder: Any feedback about release candidates should be posted with
a meaningful
Subject (not just a clone of the announcement).

We have approx. 4 weeks left until final lift-off: afterwards there
will be no
more changes on this line.



Is the OOM killer still be able to kill PolyML process for no reason? or this issue does not exist anymore with Isabelle 2021-1?

I stopped using Isabelle 2021 just because of that! It was annoying to have the same error every 5 min!

Best wishes,


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.