*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] qed and done take long for large goal states*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 10 Aug 2016 12:29:50 +0100*Cc*: Markus Wenzel <makarius at sketis.net>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <2e929697-93a4-a3d5-77c1-890fc88f4eee@inf.ethz.ch>*References*: <577E0CB2.2020109@inf.ethz.ch> <af06778a-5774-13cc-4821-f87b03e60168@sketis.net> <909629b1-c73e-4dd9-527f-57c79e4df8f8@inf.ethz.ch> <5df3b439-f029-163b-e460-713780de0d7e@sketis.net> <f02b03d5-a009-da07-14a3-092374c45dbe@inf.ethz.ch> <d1f94556-ffac-b888-5d0e-1c4f23cbd0ee@sketis.net> <19A673EB-B19F-44E5-A3F0-267E92E41669@cam.ac.uk> <2e929697-93a4-a3d5-77c1-890fc88f4eee@inf.ethz.ch>

That is a major gain and certainly worth keeping. I am not terribly bothered by the presentation of abbreviations, but nevertheless, perhaps we can get the best of both? After all, no abbreviations are printed when you type qed. Larry Paulson > On 10 Aug 2016, at 12:18, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote: > > Hi Larry, > > With the plain matching, the processing times for the qed's and done's got down from about 4.5s to 0.8s on my machine (according to the Timing panel). Since there are dozens of them in that particular theory, the effect was quite noticeable. > > Andreas > > On 10/08/16 12:27, Lawrence Paulson wrote: >> As the author of this code, which is already pretty tricky, I would be surprised if it could be fixed easily. If it were, the penalty might be much more permissive filtering, which would defeat the purpose of this code. >> >> It would be useful to see âgot indeed a bit fasterâ quantified. Did the change make a really big improvement in some situations? >> >> Larry >> >>> On 9 Aug 2016, at 22:40, Makarius <makarius at sketis.net> wrote: >>> >>> On 03/08/16 09:34, Andreas Lochbihler wrote: >>>> >>>> I manually changed the appropriate >>>> line for Isabelle2016 and processing got indeed a bit faster. >>>> >>>> Unfortunately, abbreviations are no longer contracted as they were if >>>> eta-expanded terms are involved. For example, >>>> >>>> abbreviation "rel R â list_all2 (rel_option R)" >>>> >>>> term "list_all2 (rel_option undefined)" >>>> term "list_all2 (Îx. rel_option undefined x)" >>>> >>>> Before the change, both "term" command output "rel undefined". After the >>>> change, the second prints "list_all2 (rel_option undefined)". >>> >>> This requires more rethinking of the approach. >>> >>> Net.match_term explicitly says "MUST BE BETA-ETA NORMAL", in contrast to >>> Net.unify_term. >>> >>> I am unsure if the net operations can be refined to cope with non-normal >>> terms. >>> >>> >>> Makarius >>> >>> >>

**Follow-Ups**:**Re: [isabelle] qed and done take long for large goal states***From:*Makarius

**Re: [isabelle] qed and done take long for large goal states***From:*Andreas Lochbihler

**References**:**Re: [isabelle] qed and done take long for large goal states***From:*Makarius

**Re: [isabelle] qed and done take long for large goal states***From:*Lawrence Paulson

**Re: [isabelle] qed and done take long for large goal states***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] qed and done take long for large goal states
- Next by Date: Re: [isabelle] qed and done take long for large goal states
- Previous by Thread: Re: [isabelle] qed and done take long for large goal states
- Next by Thread: Re: [isabelle] qed and done take long for large goal states
- Cl-isabelle-users August 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list