Email Gateway (Oct 05 2026 at 21:26): Email Gateway (Oct 05 2026 at 21:26):From: Makarius <makarius@sketis.net>
Another episode in the z3 story: Isabelle2026-RC3 does include arm64-darwin/z3
and thus no longer requires Rosetta 2 for anything. Although I did see many
crashes building AFP with many parallel jobs, the same happens for old
x86_64-darwin/z3. It usually works when using relatively few parallel z3
invocations.
This situation is a bit odd, and reminds us that it is better to avoid z3,
especially with the proof method (smt (z3)). There are now two alternatives:
(smt (verit)) and (smt (cvc5)). And of course, it is possible to use
sledgehammer to try on different automated proofs.
Makarius
Last updated: Oct 08 2026 at 21:07 UTC