[isabelle-dev] performance regression of typedef command

[Brian Huffman]

On Fri, Mar 26, 2010 at 1:33 PM, Makarius <makarius at sketis.net> wrote:
> On Fri, 26 Mar 2010, Brian Huffman wrote:
>
>> In Isabelle 2009, the typedef takes about 5 hundredths of a second on
>> my machine, with another few hundredths for the "by simp" part.
>>
>> In the current development version, with the new "local theory"
>> typedef package, the typedef takes nearly *half a second*.
>
> Depends what you mean by current development version.  In cef3c78ace0a it's
> not so slow anymore due to some basic tuning of type signature merge
> operations, which have been historically only used at the beginning of a
> theory but now show up whenever types are declared within a local context.

Many thanks for doing this! I tested the performance of typedef again,
and it is now back below a tenth of a second. I also tried commands
like "context field begin", and they seem to work faster now too.

- Brian