[isabelle-dev] Session builds with threads>1 but never terminates for threads=1
Fabian Huch
huch at in.tum.de
Tue Nov 14 11:00:33 CET 2023
I just encountered a theory that wouldn't terminate with threads=1, but
does so with more threads. The reason was a left-over `try` - which
obviously might not terminate, but with more than a single thread, the
rest of the session is checked, whereas with a single thread, it never
progresses (same behavior for Isabelle2023 and current devel).
Maybe it could be checked whether all commands terminate for a build,
even if they don't produce any transitions? This way we wouldn't have
this discrepancy between single-core and multi-core builds.
Fabian
More information about the isabelle-dev
mailing list