[isabelle-dev] NEWS: Nitpick/Kodkod may be invoked in the running Isabelle/Scala session
makarius at sketis.net
Fri Sep 25 16:09:53 CEST 2020
On 25/08/2020 22:06, Makarius wrote:
> *** 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.
According to experiments in the past couple of weeks, it looks good to me. So
in Isabelle/0c7a74a1c6d9 the defaults for nitpick are as follows:
kodkod_scala = true
auto_nitpick = true
If there are problems, we can reconsider it again for the coming release.
More information about the isabelle-dev