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

[Makarius]

*** 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.


	Makarius