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

[Makarius]

On Fri, 6 Nov 2015, Makarius wrote:

> On Wed, 4 Nov 2015, Clemens Ballarin wrote:
>
>>  On 30 October, 2015 20:02 CET, Makarius <makarius at sketis.net> wrote:
>> 
>> >  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.
>>
>>  Unfortunately this already fails without my patch, so it cannot be used as
>>  a test.
>
> Odd. I am in the process of looking more closely what really happens here, 
> both with and without your change.

These tests always take very long, but there is probably not much behind 
it.  Printing requires a lot of resources (space and time) and the 
timeouts are just that: the session takes very long and is interrupted.  I 
have increased some timeouts manually to get more sessions through.

Included is a slightly refined change for testing: it avoids producing a 
lot of big strings.


Since the actual change to src/Pure/Isar/generic_target.ML is so small, we 
should just go ahead with it -- after a full test with AFP.


 	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1446936258 -3600
#      Sat Nov 07 23:44:18 2015 +0100
# Node ID 8fab417a5955afbe2d211cb45d6138dd2fb880f5
# Parent  15952a05133c8b05eeadd7697333a6e70f58aeeb
test

diff -r 15952a05133c -r 8fab417a5955 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Nov 07 20:04:09 2015 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Nov 07 23:44:18 2015 +0100
@@ -588,6 +588,8 @@
     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));
+    val _ = writeln (command_msg "" tr);
+    val _ = writeln (string_of_int (length (pretty_state st')));
     val _ = get_hooks () |> List.app (fn f => (try (fn () => f tr st st') (); ()));
   in (st', opt_err') end;