Page MenuHomeIsabelle/Phabricator

Improve robustness of multithreaded Kodkod in Isabelle/Scala
Open, NormalPublic

Description

In Isabelle/0c7a74a1c6d9 enables option kodkod_scala (and auto_nitpick) by default. Thus nitpick invocations become more reactive, by reusing the already running Java process of Isabelle/Scala.

Occasional problems occur with isabelle build of Isabelle + AFP, with many parallel ML processes (e.g. -j8) sending tasks to the single managing Java process. In particular, situations of multithreaded Kodkod tasks (with interruption of parallel attempts?) seem to be prone to errors like this (seen e.g. in AFP/418c0aca9d53):

*** Unexpected outcome: "unknown"
*** At command "nitpick" (line 105 of "$AFP/Regular_Algebras/Regular_Algebras.thy")
*** Unexpected outcome: "unknown"
*** At command "nitpick" (line 101 of "$AFP/Regular_Algebras/Regular_Algebras.thy")

A temporary workaround is to switch batch sessions back to the old mode, where kodkod runs a heavy-weight Java process each time (in the session ROOT file):

options [kodkod_scala = false]

Event Timeline

makarius triaged this task as Normal priority.Oct 29 2020, 4:36 PM
makarius created this task.