Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Hi Dmitriy, Thanks for investigating. I am really surprised that the code plugin is to blame for the huge overhead. I don't know the details of the code plugin, but I have an idea of what it should do: instantiate the equals type class, register the constructors as code constructors, and declare the pattern-matching equations for case, set, rel, map and equals as [code]. None of this should involve any fancy proof. In fact, most of the equations should have already been proven by the free_constructors part or should be easily derived from them by single-step resolutions. What am I missing? Andreas On 13/04/15 12:04, Dmitriy Traytel wrote: Hi Andreas, I've investigated this a bit and the slowdown happens in the code plugin in the instantiation of the equal type class (i.e. datatype (plugins del: code) is more precise than the advice below). The number of theorems proved there is quadratic (8000 in your case). But it is still not hopeless: those 8000 theorems are proved one after each other calling Goal.prove for each of them. It is much faster to form the (balanced) conjunction, call Goal.prove (which does among other things type checking) once, and then destroy the conjunction. I'm currently testing this on testboard (http://isabelle.in.tum.de/testboard/Isabelle/rev/1863cdff2010). Cheers, Dmitriy On 09.04.2015 16:11, Andreas Lochbihler wrote: Hi Dmitriy and Jasmin, Thanks for the hint with plugins. That really speeds things up. I also suspect that the timing panel does not include the forked proof tactics. Cheers, Andreas On 09/04/15 15:55, Dmitriy Traytel wrote: Hi Andreas, rather than going dirty, try: datatype (plugins only:) family ... It seems that here we are lucky and the slowdown is caused by one of the plugins. (We'll investigate which one.) Cheers, Dmitriy PS: Your datatype reminded me of another one, which allows (or allowed) proving False in a different theorem prover ;-) https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html On 09.04.2015 15:44, Jasmin Blanchette wrote: Hi Andreas, In Isabelle2014, processing this datatype declaration takes about one minute. So what has happened in between? (The Isabelle2014 timing panel is also way off with 8 seconds.) Thanks for your report. What happened in between is that we generate more theorems. I suspect one or a few of them have tactics that scale poorly (e.g. cubic) in the number of constructors. As for the timing panel, I suspect it does not take into consideration the time spent in tactics with multithreading on, but I’m not an expert there. We’ll look into this. You could try “quick_and_dirty” around that particular datatype to make things more tolerable in the meantime. Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Hi Dmitriy, the code plugin defines a new constant (copy of op =) that is used as equality. datatype x = A | B export_code equal_x_inst.equal_x in SML This is precisely the instantiation of the equals type class. To get it executable (#constructors)^2 equations are proved in a backward fashion (I'm sure it could be easilly done in a forward fashion as well). However, this code goes back to Stefan and Florian, and we didn't attempt to optimize it when integrating it with the new package. I see. But isn't the performance now (894d6d863823 ) already acceptable? I have not tried it yet, because I am busy testing Isabelle2015-RC0. Cheers, Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Hi Andreas, the code plugin defines a new constant (copy of op =) that is used as equality. datatype x = A | B export_code equal_x_inst.equal_x in SML To get it executable (#constructors)^2 equations are proved in a backward fashion (I'm sure it could be easilly done in a forward fashion as well). However, this code goes back to Stefan and Florian, and we didn't attempt to optimize it when integrating it with the new package. But isn't the performance now (894d6d863823 ) already acceptable? Dmitriy On 14.04.2015 08:10, Andreas Lochbihler wrote: Hi Dmitriy, Thanks for investigating. I am really surprised that the code plugin is to blame for the huge overhead. I don't know the details of the code plugin, but I have an idea of what it should do: instantiate the equals type class, register the constructors as code constructors, and declare the pattern-matching equations for case, set, rel, map and equals as [code]. None of this should involve any fancy proof. In fact, most of the equations should have already been proven by the free_constructors part or should be easily derived from them by single-step resolutions. What am I missing? Andreas On 13/04/15 12:04, Dmitriy Traytel wrote: Hi Andreas, I've investigated this a bit and the slowdown happens in the code plugin in the instantiation of the equal type class (i.e. datatype (plugins del: code) is more precise than the advice below). The number of theorems proved there is quadratic (8000 in your case). But it is still not hopeless: those 8000 theorems are proved one after each other calling Goal.prove for each of them. It is much faster to form the (balanced) conjunction, call Goal.prove (which does among other things type checking) once, and then destroy the conjunction. I'm currently testing this on testboard (http://isabelle.in.tum.de/testboard/Isabelle/rev/1863cdff2010). Cheers, Dmitriy On 09.04.2015 16:11, Andreas Lochbihler wrote: Hi Dmitriy and Jasmin, Thanks for the hint with plugins. That really speeds things up. I also suspect that the timing panel does not include the forked proof tactics. Cheers, Andreas On 09/04/15 15:55, Dmitriy Traytel wrote: Hi Andreas, rather than going dirty, try: datatype (plugins only:) family ... It seems that here we are lucky and the slowdown is caused by one of the plugins. (We'll investigate which one.) Cheers, Dmitriy PS: Your datatype reminded me of another one, which allows (or allowed) proving False in a different theorem prover ;-) https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html On 09.04.2015 15:44, Jasmin Blanchette wrote: Hi Andreas, In Isabelle2014, processing this datatype declaration takes about one minute. So what has happened in between? (The Isabelle2014 timing panel is also way off with 8 seconds.) Thanks for your report. What happened in between is that we generate more theorems. I suspect one or a few of them have tactics that scale poorly (e.g. cubic) in the number of constructors. As for the timing panel, I suspect it does not take into consideration the time spent in tactics with multithreading on, but I’m not an expert there. We’ll look into this. You could try “quick_and_dirty” around that particular datatype to make things more tolerable in the meantime. Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: powr
On Sun, 12 Apr 2015, Larry Paulson wrote: You should always have success by unfolding powr_def. And I’m told that the necessary changes to “approximation” are not difficult. Does that mean there will be further changes, to make it fully work in the coming release? It would be nice to see this last-minute change properly stabilized, such that Isabelle does not degrade into continuous non-release repository-snapshot quality, like so many other projects today. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s
Hi Dmitriy, However, this code goes back to Stefan and Florian, and we didn't attempt to optimize it when integrating it with the new package. don't blame Stefan for that ;-). Proving equations for equality was the first deductive plugin I ever wrote and it has hardly changed over the years. Thanks for your effort, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Local_Theory.open_target instead of Local_Theory.restore
On Sun, 12 Apr 2015, Florian Haftmann wrote: I have done a grep on this: src/Pure/Isar/named_target.ML:197: (Context.Proof o Local_Theory.restore, lthy) This is the only place where Local_Theory.restore is used according to its original idea. It might be possible to get rid of it eventually, like the old reinit, but it is not a big deal. src/HOL/Library/bnf_axiomatization.ML:84: || `Local_Theory.restore; src/HOL/Tools/BNF/bnf_def.ML:794:? Local_Theory.restore; ... src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML:633:|| `Local_Theory.restore; That is all about BNF, and Dmitriy has already said that he will continue work there after the relase. Eliminating Local_Theory.restore will make it possible to use private datatype for example, and get the expected effect on the name space entries. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New proof method rewrite
On 09.04.2015 21:08, Makarius wrote: On Thu, 9 Apr 2015, Lars Noschinski wrote: On 18.03.2015 15:16, Lars Noschinski wrote: commit 4ed50ebf5d36 adds a new proof method rewrite. This is the pattern-based replacement for subst Christoph Traut and I presented at the last Isabelle Workshop [1]. For now, it lifes in ~~/src/HOL/Library/Rewrite and is still missing a proper documentation (but there are examples in ~~/src/HOL/ex/Rewrite_Examples). I've used it now a bit to add annotations in program verification and (contrary to my former intuition) found the order of the patterns to be the wrong way around. If someone has used the rewrite method and has some opinions on that, I would be glad to hear these. I haven't used it yet, although I looked a bit through the sources, just as a matter of pre-release routine. I also added a symbol assignment for \hole in the IsabelleText font and isabellesym.sty -- it is the result of spending 30min looking carefully through DejaVuSansMono and http://mirrors.ctan.org/info/symbols/comprehensive/symbols-a4.pdf -- see now b911c8ba0b69. LaTeX packages should not be overly exotic as rendering of Isabelle symbols -- hopefully wasysym.sty was a decent choice here. Nice, this deals with the conflict I encountered a few days ago with the use of the \box symbol in AutoCorres. Back to the actual topic of this thread: If you want to change the syntax for the release, there are a very few days left until the first release candidate is published, while the repository still remains in pre-forked state, probably until the end of next week. Technically, to have Parse.xthms1 before quasi-keywords like at, you need some Scan.unless trickery, but it should be doable. Method.sections also manages that with add, del etc. I was not clear above. I don't want to change the general syntax of position to rules, but was contemplating whether the position should read inside-out or outside-in. As I noted in my other mail, this will have to wait for the next round. Here is also a command line to explore possibilities of true keywords, instead of quasi-keywords: $ isabelle build -n -a -d '$AFP' -k at -k asm -k concl Note that outer syntax is now local to each theory, so as long as it is just a separate theory somewhere, one can be liberal. Anything for main HOL needs more care, of course. (For Eisbach we also have some open problems with keyword clashes still left to address, concl is one of them.) The goal is definitely to have the tool end up in Main, so I will not get too fancy with the syntax. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New proof method rewrite
On Thu, 9 Apr 2015, Makarius wrote: Back to the actual topic of this thread: If you want to change the syntax for the release, there are a very few days left until the first release candidate is published Is there still anything coming for the release on this thread? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Z3 open source
On Wed, 8 Apr 2015, Jasmin Blanchette wrote: - Z3 is now always enabled by default, now that it is fully open source. The z3_non_commercial option is discontinued. In addition, Z3 should now (again) be invoked by default by Sledgehammer. Let me know if you see anything odd, e.g. odd problems with binaries on Linux or Windows. What is still not clear to me is how provers are determined. The Sledgehammer panel uses the system option sledgehammer_provers, after many failed attempts in the past to cope with the ML heuristics. In Isabelle/323feed18a92 I've tried to update this wrt. recent changes. Is it true that E prover now has this low priority in the list? It was once first, IIRC. Moreover, in Isabelle/dda1e781c7b4 I've updated the NEWS to say explicitly that the scheduling for provers managed by the Sledgehammer panel should now work better wrt. ongoing edits. Despite such routine improvements, many users will probably just stick to old habits from the TTY age, and put the sledgehammer command into the text. (Are there remaining uses of this ancient form? Or are there still pending problems with the current Sledgehammer panel?) BTW, the Sledgehammer manual still describes a situation before the Sledgehammer panel came into existance in 2013. (It mentions the earlier Auto Sledgehammer in PIDE, though.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
