On Wed, 4 Nov 2015, Clemens Ballarin wrote:
On 30 October, 2015 20:02 CET, Makarius <makar...@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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
