Re: [isabelle] Performance bottleneck in Theory_Data.merge





On 13. Jul 2021, at 17:44, Thomas Sewell <tals4 at cam.ac.uk> wrote:

If you're very keen to figure it out, I'd be tempted to locally edit
context.ML to expose an alternative interface to Theory_Data that lets
the client suggest a name which appears with the position info in timing.

I followed your advice and manually named all data. Here is what I found:

1. The inefficient data is in locale.ML, namely: structure Thms. Sets of theorems are represented as lists there. Changing this to Thmtab.set, and doing a pointer_eq test on merge seems to solve my performance issue.

2. Whether position information is displayed or not seems to depend on how the structure is actually generated, ie.
via. Theory_Data’, Theory_Data, or Generic_Data and also how the arguments are declared. Some observations:
* Theory_Data’ seems to result in a filename as position
* Generic_Data(struct Type T = … end) seems to result in a link as position
* Generic_Data(Type T = …) (without the explicit struct) seems to have no position information.


Regards,
Norbert

--

Norbert Schirmer (nschirmer at apple.com)
 SEG Formal Verification



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.