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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
