*** 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
