[isabelle-dev] syntax errors cause hanging

[Lawrence Paulson]

I think I've worked this out. Something was looping in a parallel thread probably.
Larry

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.
> 
> Larry
> 
> ~/isabelle/Repos/src/ZF: isabelle makemake[2]: Nothing to be done for `Pure'.
> Building ZF ...
> ^CZF FAILED
> (see also /Users/lp15/isabelle/Repos/heaps/polyml-5.4.0_x86-darwin/log/ZF)
> 
> *** Theory loader: failed to load "Main" (unresolved "Main_ZF")
> *** Theory loader: failed to load "AC" (unresolved "Main_ZF")
> *** Theory loader: failed to load "Zorn" (unresolved "AC")
> *** Theory loader: failed to load "Cardinal_AC" (unresolved "Zorn")
> *** Theory loader: failed to load "InfDatatype" (unresolved "Cardinal_AC")
> *** Theory loader: failed to load "Main_ZFC" (unresolved "Main_ZF", "InfDatatype")
> *** Theory loader: undefined theory entry for "pair"
> *** Theory loader: undefined theory entry for "equalities"
> *** Outer syntax error (line 26 of "~~/src/ZF/Bin.thy"): command expected,
> *** but symbolic identifier \<or> (line 26 of "~~/src/ZF/Bin.thy") was found
> *** At command "<malformed>" (line 24 of "~~/src/ZF/Bin.thy")
> *** Outer syntax error (line 14 of "~~/src/ZF/List_ZF.thy"): command expected,
> *** but symbolic identifier \<or> (line 14 of "~~/src/ZF/List_ZF.thy") was found
> *** At command "<malformed>" (line 13 of "~~/src/ZF/List_ZF.thy")
> *** Failed to finish proof
> *** At command "by" (line 80 of "~~/src/ZF/pair.thy")
> *** Failed to finish proof
> *** At command "by" (line 334 of "~~/src/ZF/upair.thy")
> Exception- TOPLEVEL_ERROR raised
> *** ML error
>