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

Makarius makarius at sketis.net
Fri Nov 6 11:20:13 CET 2015

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.


More information about the isabelle-dev mailing list