Re: [isabelle] Performance bottleneck in Theory_Data.merge



(This rather old thread still requires more comments.)

On 14/07/2021 18:26, Norbert Schirmer via Cl-isabelle-users wrote:
> 
> 
>> On 13. Jul 2021, at 17:44, Thomas Sewell <tals4 at cam.ac.uk
>> <mailto: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.

I have already changed that some weeks ago, to use more scalable data
structures. See
https://isabelle-dev.sketis.net/rISABELLEc3b3517ef4ba

Note that thm Item_Net.T preserves the original "canonical order of
declarations": it is an index structure paired with a plain list; thus I don't
have to argue if the order matters or not. (A minor disadvantage is that the
net produces more heap garbage, so in extreme applications it might need to be
revisited.)


> 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.

I could not reproduce this observation.


	Makarius




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