Email Gateway (Oct 01 2026 at 15:47): Email Gateway (Oct 01 2026 at 15:47):From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] RC1: Experience report from porting two big projects to RC1
Dear list,
I've ported Isabelle LLVM and our parallel Bernoulli Number computation
from 2025-2 to RC2. No bigger issues to report, apart from a
sledgehammer anomaly that I reported in a separate message.
--
Peter
largely straightforward. Discontinued addsimps is a bit annoying, but
just reoplacing it with |> Simplifier.add_simps works in many cases,
otherwise add () around argument.
Ran into sledgehammer problem when using is present, reported separately.
Noticed that sledgehammmer now generates using for local facts
itself: nice!
The warning on strings that look like formal names "foo.bar" is nice!
Using \verbatim to disable, for eg LLVM-intrinsic names, is not too much
of a pain. And I found one spot where I actually am using formal
names as a string ;)
Some function, eg in Specification, got a verbose-option. It's not
clear to me what that does, I set it to false analogously to such
changes in AFP.
bernoulli_rat is gone: awkward type-annot adding (but probably there
are easier ways to fix the proof)
otherwise, straightforward, and most problems where caused by, at the
same time, switching to a new version of Isabelle LLVM that has slightly
different rules for the refinement of sequential by parallel code
(dynamic-assertion support required this change).
Last updated: Oct 08 2026 at 21:07 UTC