[isabelle] RC5: Short experience report

Hi List.

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
unrecoverable grey-out.
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
> https://isabelle.sketis.net/website-Isabelle2021-RC5
> See again
> https://isabelle-dev.sketis.net/phame/post/view/28/release_candidates_for_isabelle2021
> and 4 for further details.
> Any feedback about release candidates should be posted with a
> meaningful
> Subject including the version (not just a clone of this
> announcement).
> People who have tested earlier release candidates should definitely
> follow
> this one, otherwise some last-minute problems might remain
> undetected.
> 	Makarius

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