On Thu, 29 Oct 2015, Florian Haftmann wrote:
I have not spend any thoughts whether there could be terminaton issues.
Is there any argument beyond the absence of counterexamples that that
can never happen?
Standard batch build prints relatively few terms, so this is not yet
significant as a test.
The following change prints every intermediate Isar toplevel state. With
that I get timeouts or interrupts due to out-of-memory situation in
various sessions, e.g. HOL-Nominal-Examples or Jinja.
I did not look what really happens.
This is Isabelle/d05f3d86a758 and AFP/20f80d4c7850.
Makarius# HG changeset patch
# User wenzelm
# Date 1446231391 -3600
# Fri Oct 30 19:56:31 2015 +0100
# Node ID 75fa4c345fc77dbd8b5621205ed620f484896b6d
# Parent d05f3d86a758931d5cd379b9ec86b766eebb20da
test
diff -r d05f3d86a758 -r 75fa4c345fc7 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML Fri Oct 30 17:14:30 2015 +0100
+++ b/src/Pure/Isar/toplevel.ML Fri Oct 30 19:56:31 2015 +0100
@@ -585,6 +585,7 @@
val (st', opt_err) =
Context.setmp_thread_data (try (Context.Proof o presentation_context_of)
st)
(fn () => app int tr st) ();
+ val _ = writeln (string_of_state st');
val opt_err' = opt_err |> Option.map
(fn Runtime.EXCURSION_FAIL exn_info => exn_info
| exn => (Runtime.exn_context (try context_of st) exn, at_command tr));
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
