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

[Makarius]

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.


	Makarius