On Fri, 6 Nov 2015, Makarius wrote:
On Wed, 4 Nov 2015, Clemens Ballarin wrote:
On 30 October, 2015 20:02 CET, Makarius 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.
> 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
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# 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;
isabelle-dev mailing list