Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Any fans of "try"?


view this post on Zulip Email Gateway (Jan 03 2021 at 11:53):

From: Makarius <makarius@sketis.net>
I was experimenting with auto_nitpick for Isabelle2021, but have disabled it
for Isabelle2021-RC1, see also
https://isabelle-dev.sketis.net/rISABELLE52ba78df4088 "disable auto_nitpick
for now: spurious problems with non-termination e.g. in HOL-Hoare examples".

The deeper problem behind it is the new Isabelle/Scala implementation of
Kodkod: it sometimes has problems with parallelism and interrupts.

The old external Java process for Kodkod is still there, and actually used by
default in "isabelle build" (for robustness and conservatity). Using it in
auto-mode is not feasible, especially on Windows.

At some point I would like to get Isabelle/Scala Kodkod into proper form as
the only version of that tool, see also https://isabelle.sketis.net/repos/kodkodi

Then we could also reconsider the auto_nitpick option.

(This is not relevant for the Isabelle2021 release in February, but maybe for
the one 8-10 months later.)

Makarius


Last updated: Mar 29 2024 at 08:18 UTC