[isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
makarius at sketis.net
Sat Nov 7 23:52:16 CET 2015
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.
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1446936258 -3600
# Sat Nov 07 23:44:18 2015 +0100
# Node ID 8fab417a5955afbe2d211cb45d6138dd2fb880f5
# Parent 15952a05133c8b05eeadd7697333a6e70f58aeeb
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;
More information about the isabelle-dev