[isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
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