Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Session builds with threads>1 but never te...


view this post on Zulip Email Gateway (Nov 14 2023 at 10:00):

From: Fabian Huch <huch@in.tum.de>
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


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

view this post on Zulip Email Gateway (Nov 14 2023 at 10:50):

From: Lawrence Paulson <lp15@cam.ac.uk>
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.

Larry


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


Last updated: Mar 04 2024 at 10:08 UTC