[isabelle-dev] NEWS: Nitpick/Kodkod may be invoked in the running Isabelle/Scala session

Makarius makarius at sketis.net
Tue Aug 25 22:06:29 CEST 2020

*** HOL ***

* Nitpick/Kodkod may be invoked directly within the running
Isabelle/Scala session (instead of an external Java process): this
improves reactivity and saves resources. This experimental feature is
guarded by system option "kodkod_scala" (default: false).

This refers to Isabelle/5c057abc1b78.

I have made some basic tests to see that it works in batch builds and in

Early adopters are encouraged to try it out by enabling option "kodkod_scala",
e.g. via the Plugin Options menu in Isabelle/jEdit.

Potential problems to watch out for:

  * Overloading the Java process that runs Isabelle/Scala/PIDE by Kodkod tasks
that are not properly interrupted, or require too many resources.

  * Instabilities of Kodkod tasks that invoke external solvers as JNI
libraries within the same Java process.

It might also make sense to experiment with auto_nitpick enabled.


More information about the isabelle-dev mailing list