[isabelle-dev] syntax errors cause hanging

[Makarius]

> 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