[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