[isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Makarius]

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
-------------- next part --------------
# 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));