On 6 Mar 2012, at 12:00, Lawrence Paulson wrote:
I remember when you could build a logic by typing “isabelle make", and
if an error occurred somewhere, it would terminate with an error
message.
I am trying to make textual changes now, and I find that “isabelle
make" simply hangs. if I terminate it, I discover where I have
introduced some sort of syntax error. See the attached text.
Why can't it terminate upon reaching an error, like before? It's not in
a loop. PG similarly hangs and must be killed.
On Tue, 6 Mar 2012, Lawrence Paulson wrote:
I think I've worked this out. Something was looping in a parallel thread
probably. Larry
The question here is about the meaning of failing or diverging
computations in parallel Isabelle/ML. When you load a bunch of theories,
say via some import of a sub-graph in the theory header, the system
conceptually does a join of all pending tasks emerging from it. If one of
the tasks loops, the join never finishes.
If you now inject an interrupt into the whole process, all current and
future tasks will enter a failed state, and the pending join will result
in the set of genuine errors accumulated so far -- filtering out
meaningless Interrupt exceptions.
I've made some sanity checks in current Isabelle/9b38f8527510, in batch
mode, Proof General, and Isabelle/jEdit. Results are non-deterministic
but make sense within the usual boundaries. In particular, I did not see
PG hanging -- its kill switch managed to abort the current attempt to load
various theories in parallel.
In Isabelle/jEdit the situation is even better, because the GUI gives
early feedback on individual failures while other tasks crunch (or loop).
But there are still technical limitations in the visibility of this in the
status panel -- apart from the pain to bootstrap ZF in the editor due to
its newly defined Isar commands.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
