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

Makarius 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
> Isabelle/jEdit.
> 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 mailing list