[isabelle-dev] Session builds with threads>1 but never terminates for threads=1

Lawrence Paulson lp15 at cam.ac.uk
Tue Nov 14 11:49:57 CET 2023

Sure, if there is a way to accomplish that. Probably it's much easier to scan for stray occurrences of such commands in a theory. 


> On 14 Nov 2023, at 10:00, Fabian Huch <huch at in.tum.de> wrote:
> 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.

More information about the isabelle-dev mailing list