[isabelle] RC5: Short experience report
I have now ported a big chunk of Isabelle-LLVM to RC5.
Notably, Isabelle-LLVM extensively uses the Word library, and also
contains some lower-level Isabelle-ML code.
First, Isabelle seems to run stable. I did not run into any
It was killed one time by my OOM killer, but I had two instances in
parallel on 32GB RAM.
With the NEWS file, and a bit of guessing, the Isabelle-ML code was
easily ported, most severe problem was the undocumented change
Path.smart_implode -> Path.implode_symbolic.
Porting of lemmas using the word library was, as expected, more
difficult. With the help of sledgehammer, which feels really powerful,
I could force most lemmas through, even without a complete
understanding or overview of the changes to Word.
On Mon, 2021-02-08 at 22:42 +0100, Makarius wrote:
> Dear Isabelle users,
> the end of the Isabelle2021 release process is getting pretty close.
> Presumably the last release candidate is
> See again
> and 4 for further details.
> Any feedback about release candidates should be posted with a
> Subject including the version (not just a clone of this
> People who have tested earlier release candidates should definitely
> this one, otherwise some last-minute problems might remain
This archive was generated by a fusion of
Pipermail (Mailman edition) and