Re: [isabelle] Performance bottleneck in Theory_Data.merge
- To: Norbert Schirmer <nschirmer at apple.com>, Thomas Sewell <tals4 at cam.ac.uk>
- Subject: Re: [isabelle] Performance bottleneck in Theory_Data.merge
- From: Makarius <makarius at sketis.net>
- Date: Wed, 22 Sep 2021 13:03:12 +0200
- Authentication-results: cam.ac.uk; iprev=pass (mta2.cl.cam.ac.uk) smtp.remote-ip=126.96.36.199; spf=softfail smtp.mailfrom=sketis.net; dkim=pass header.d=sketis.net header.s=key2 header.a=rsa-sha256; arc=none
- Authentication-results: cam.ac.uk; iprev=pass (relay.yourmailgateway.de) smtp.remote-ip=188.8.131.52; spf=pass smtp.mailfrom=sketis.net; dkim=pass header.d=sketis.net header.s=key2 header.a=rsa-sha256; arc=none
- Authentication-results: mx2f26; spf=pass (sender IP is 184.108.40.206) smtp.mailfrom=makarius at sketis.net smtp.helo=[192.168.179.20]
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>, Sebastian Skalberg <skalberg at apple.com>
- In-reply-to: <40DEAAC4-8FB9-458B-B4C9-28557DE4627F@apple.com>
- References: <E38D033E-29E5-41F9-A61F-29F963DCCC9B@apple.com> <firstname.lastname@example.org> <40DEAAC4-8FB9-458B-B4C9-28557DE4627F@apple.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.13.0
(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
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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and