Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Nitpick/Kodkod may be invoked in the...

Email Gateway (Aug 25 2020 at 20:06):

From: Makarius <makarius@sketis.net>
* 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
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Sep 25 2020 at 14:10):

From: Makarius <makarius@sketis.net>
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

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Feb 01 2025 at 20:19 UTC