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 > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev