Re: [isabelle-dev] HOL-Proofs broken?
> On 06.10.2015, at 22:55, Jasmin Blanchette wrote: > > The problem is most likely caused by ebf296fe88d7. Looking at it more > closely, one sees a proof that is (at least) quadratic in the number of > constructors: > >fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts > rel_distincts rel_eqs = > HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) > THEN_ALL_NEW >rtac ctxt (infer_instantiate' ctxt [SOME ct2] exhaust) THEN_ALL_NEW > > I would not exclude that this could give rise to some big proof objects in > conjunction with a type like "nibble", for which we previously did not > generate the "case_transfer" rule (nor "rel_cases" upon which it relies). My suspicion appears to have been correct. I am now able to build "HOL-Proofs" in 13 min on my MacBook Pro. (I have no idea why my test of 5b5656a63bd6 "diverged" yesterday.) I'm now testing everything and will push once this is done. Sorry for the trouble. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs broken?
> On 06.10.2015, at 22:37, Makarius wrote: > >> On Tue, 6 Oct 2015, Dmitriy Traytel wrote: >> >> So the main candidates for bad changesets are: ebf296fe88d7, 2ebdd603cd71. > > More results on macbroy2: > > 5b5656a63bd6 > Finished HOL-Proofs (0:18:14 elapsed time, 0:49:28 cpu time, factor 2.71) > > 2ebdd603cd71 > Building HOL-Proofs ... > Warning - Unable to increase stack - interrupting thread > Warning - Unable to increase stack - interrupting thread > *** Interrupt The problem is most likely caused by ebf296fe88d7. Looking at it more closely, one sees a proof that is (at least) quadratic in the number of constructors: fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs = HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW rtac ctxt (infer_instantiate' ctxt [SOME ct2] exhaust) THEN_ALL_NEW I would not exclude that this could give rise to some big proof objects in conjunction with a type like "nibble", for which we previously did not generate the "case_transfer" rule (nor "rel_cases" upon which it relies). Let me look into this. It might take a bit of time before I sort this all out, but hopefully we'll be back to normal tomorrow (Wednesday). Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs broken?
On Tue, 6 Oct 2015, Makarius wrote: On Tue, 6 Oct 2015, Dmitriy Traytel wrote: As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about 17 minutes. This conforms to my expectations: HOL-Proofs is slow, but works. I am presently on a side-branch starting from 5b5656a63bd6, and that works as well: https://bitbucket.org/makarius/isabelle/commits/1727d7d14d76 So the main candidates for bad changesets are: ebf296fe88d7, 2ebdd603cd71. More results on macbroy2: 5b5656a63bd6 Finished HOL-Proofs (0:18:14 elapsed time, 0:49:28 cpu time, factor 2.71) 2ebdd603cd71 Building HOL-Proofs ... Warning - Unable to increase stack - interrupting thread Warning - Unable to increase stack - interrupting thread *** Interrupt Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs broken?
On Tue, 6 Oct 2015, Dmitriy Traytel wrote: As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about 17 minutes. This conforms to my expectations: HOL-Proofs is slow, but works. I am presently on a side-branch starting from 5b5656a63bd6, and that works as well: https://bitbucket.org/makarius/isabelle/commits/1727d7d14d76 So the main candidates for bad changesets are: ebf296fe88d7, 2ebdd603cd71. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs broken?
As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about 17 minutes. Timing = :threads=4elapsed=979.269cpu=2582.077gc=323.518factor=2.64 Dmitriy > On 06 Oct 2015, at 21:54, Jasmin Blanchette > wrote: > > Hi Makarius, > >> My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out >> of resources and fail. I've made approx. 3 runs in the vicinity -- it >> always takes very long. >> >> Is that another failure to do a full "isabelle build -a" before pushing >> anything? > > I did "isabelle build -a" but stopped after some time because "HOL-Proofs" > diverged. Then I went back to the last repository version and had exactly the > same divergence behavior. Testboard is down, and if my 2015 MacBook Pro can't > do it, we have a problem, already before ebf296fe88d7. > > 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] HOL-Proofs broken?
Hi Makarius, > My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out of > resources and fail. I've made approx. 3 runs in the vicinity -- it always > takes very long. > > Is that another failure to do a full "isabelle build -a" before pushing > anything? I did "isabelle build -a" but stopped after some time because "HOL-Proofs" diverged. Then I went back to the last repository version and had exactly the same divergence behavior. Testboard is down, and if my 2015 MacBook Pro can't do it, we have a problem, already before ebf296fe88d7. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] HOL-Proofs broken?
My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out of resources and fail. I've made approx. 3 runs in the vicinity -- it always takes very long. Is that another failure to do a full "isabelle build -a" before pushing anything? I've actually violated this principle myself, and pushed a696414fa3a1 over it, which is a change of some Admin/isatest configuration, but that is a different story. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs
On Wed, 14 May 2014, Tobias Nipkow wrote: This is what I did interactively: starting from Pure I loaded Proofs.thy first and then Main.thy. Maybe this did not really switch proof terms on? That should do the right thing. The remaining explanation is that PIDE is less aggressive in proof parallelization and less heap was used. That performance profile is specific to for HOL-Proofs: more parallelism requires more space, and some years ago HOL-Proofs actually had parallel_proofs = 0. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs
On 14/05/2014 16:06, Makarius wrote: > On Wed, 14 May 2014, David Matthews wrote: > >> I don't know why it should be different when you run it interactively. > > That is just because an interactive PIDE session is quite different from a > batch > build session it what it does. I've tries for years to unify that further, > but > we are actually moving away from it. > > Normally PIDE interaction requires more resources than batch build. For > HOL-Proofs I suspect that Tobias did not have the proofs enabled, because that > requires some special tricks in its bootstrap. In contrast, using isabelle > jedit -l HOL-Proofs or equivalent should to the right thing, and enable the > proof terms, but the critical phase is already over at that point. This is what I did interactively: starting from Pure I loaded Proofs.thy first and then Main.thy. Maybe this did not really switch proof terms on? Tobias > >> I would assume that you are running in 32-bit mode. Have you tried in 64-bit >> mode with a larger heap? > > Our usual defaults are for 32-bit mode, which normally works thanks to the > online heap sharing. > > The move to 64-bit will be inevitable at some point, especially for bigger > applications that live on the edge of what is possible -- although main HOL > itself is already close to that. 64-bit means that people cannot use small > mobile devives anymore, with only 4-8 GB, but require a real machine with 16 > GB > or more. > > See also this related thread > http://www.mail-archive.com/isabelle-dev%40mailbroy.informatik.tu-muenchen.de/msg04536.html > > > In fact, polyml-5.5.2 from Isabelle/e7bf30290627 might already circumvent that > particular problem from last September, although but I have seen other > situations of hitting the wall for AFP/Collections and related sessions with > 5.5.2 as approximated from the SVN version in the past few months. > > > Makarius > ___ > 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] HOL-Proofs
On Wed, 14 May 2014, David Matthews wrote: I don't know why it should be different when you run it interactively. That is just because an interactive PIDE session is quite different from a batch build session it what it does. I've tries for years to unify that further, but we are actually moving away from it. Normally PIDE interaction requires more resources than batch build. For HOL-Proofs I suspect that Tobias did not have the proofs enabled, because that requires some special tricks in its bootstrap. In contrast, using isabelle jedit -l HOL-Proofs or equivalent should to the right thing, and enable the proof terms, but the critical phase is already over at that point. I would assume that you are running in 32-bit mode. Have you tried in 64-bit mode with a larger heap? Our usual defaults are for 32-bit mode, which normally works thanks to the online heap sharing. The move to 64-bit will be inevitable at some point, especially for bigger applications that live on the edge of what is possible -- although main HOL itself is already close to that. 64-bit means that people cannot use small mobile devives anymore, with only 4-8 GB, but require a real machine with 16 GB or more. See also this related thread http://www.mail-archive.com/isabelle-dev%40mailbroy.informatik.tu-muenchen.de/msg04536.html In fact, polyml-5.5.2 from Isabelle/e7bf30290627 might already circumvent that particular problem from last September, although but I have seen other situations of hitting the wall for AFP/Collections and related sessions with 5.5.2 as approximated from the SVN version in the past few months. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs
On 13/05/2014 17:18, Makarius wrote: On Tue, 13 May 2014, Tobias Nipkow wrote: I added a few lemmas to List and now the HOL-Proofs session no longer terminates. This is what I got to see when I interrupted one run: ^Cpoly(52110,0xb0185000) malloc: *** mach_vm_map(size=8388608) failed (error code=3) *** error: can't allocate region *** set a breakpoint in malloc_error_break to debug *** Interrupt HOL-Proofs FAILED When I load the session interactively, I don't have a problem. Any hints what I should be doing? That is a Poly/ML heap allocation problem specifically on Mac OS X. David Matthews has occasionally explained the technical side-conditions imposed by Apple, but I did not really understand them. On its own this is at most a warning. If the ML application requires a large heap Poly/ML tries to allocate as much memory as it can. There is no way to find out how much free space is left so this sometimes involves making allocation requests and testing the result to see if they have succeeded. If a call fails Poly/ML recovers from it. That is perfectly normal. Other operating systems simply return a failure result in these circumstances but for some reason Apple have decided to print this message as well. It typically appears in 32-bit mode when the maximum address space has been reached. That, though is a separate issue from why the session does not terminate. The most likely explanation is that it requires more memory than is available and the garbage-collector can't keep up. I don't know why it should be different when you run it interactively. I would assume that you are running in 32-bit mode. Have you tried in 64-bit mode with a larger heap? David ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs
It seems that I have the same problem, because the 2 lemmas I added also use metis. Playing around with system parameters does not do anything. Tobias On 14/05/2014 00:32, Ondřej Kunčar wrote: > I also had a similar problem some time ago and I solved it by changing the > proof. You can get by bisecting to the very point that makes HOL-Proofs choke > and change it. I am not sure anymore but I think in my example I just changed > metis for blast or something like this. > > Ondrej > > On 05/13/2014 06:08 PM, Tobias Nipkow wrote: >> I added a few lemmas to List and now the HOL-Proofs session no longer >> terminates. This is what I got to see when I interrupted one run: >> >> ^Cpoly(52110,0xb0185000) malloc: *** mach_vm_map(size=8388608) failed (error >> code=3) >> *** error: can't allocate region >> *** set a breakpoint in malloc_error_break to debug >> *** Interrupt >> HOL-Proofs FAILED >> >> When I load the session interactively, I don't have a problem. Any hints >> what I >> should be doing? >> >> Tobias >> ___ >> 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs
I also had a similar problem some time ago and I solved it by changing the proof. You can get by bisecting to the very point that makes HOL-Proofs choke and change it. I am not sure anymore but I think in my example I just changed metis for blast or something like this. Ondrej On 05/13/2014 06:08 PM, Tobias Nipkow wrote: I added a few lemmas to List and now the HOL-Proofs session no longer terminates. This is what I got to see when I interrupted one run: ^Cpoly(52110,0xb0185000) malloc: *** mach_vm_map(size=8388608) failed (error code=3) *** error: can't allocate region *** set a breakpoint in malloc_error_break to debug *** Interrupt HOL-Proofs FAILED When I load the session interactively, I don't have a problem. Any hints what I should be doing? Tobias ___ 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] HOL-Proofs
On Tue, 13 May 2014, Tobias Nipkow wrote: I added a few lemmas to List and now the HOL-Proofs session no longer terminates. This is what I got to see when I interrupted one run: ^Cpoly(52110,0xb0185000) malloc: *** mach_vm_map(size=8388608) failed (error code=3) *** error: can't allocate region *** set a breakpoint in malloc_error_break to debug *** Interrupt HOL-Proofs FAILED When I load the session interactively, I don't have a problem. Any hints what I should be doing? That is a Poly/ML heap allocation problem specifically on Mac OS X. David Matthews has occasionally explained the technical side-conditions imposed by Apple, but I did not really understand them. I usually just tinker with ML_OPTIONS in $ISABELLE_HOME/etc/settings until it works again. Here is an arbitrary example: ML_OPTIONS="--minheap 800 --maxheap 3000 --gcthreads 4" It depends on your hardware what makes sense, and on some luck what works. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] HOL-Proofs
I added a few lemmas to List and now the HOL-Proofs session no longer terminates. This is what I got to see when I interrupted one run: ^Cpoly(52110,0xb0185000) malloc: *** mach_vm_map(size=8388608) failed (error code=3) *** error: can't allocate region *** set a breakpoint in malloc_error_break to debug *** Interrupt HOL-Proofs FAILED When I load the session interactively, I don't have a problem. Any hints what I should be doing? Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs slow
>> As a first step, cf. the following changeset: >> >>> http://isabelle.in.tum.de/reports/Isabelle/rev/8b50286c36d3 > > Testing this verson manually gives me 0:25:05 elapsed time total, while > it is normally 0:16:30 on this machine with 8 cores and "build -j4 -a". http://isabelle.in.tum.de/reports/Isabelle/rev/f11f8905d9fd eliminates the code_simp invocations by more elementary proofs. 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] HOL-Proofs slow
On Mon, 22 Oct 2012, Florian Haftmann wrote: Bijection then produced this: The first bad revision is: changeset: 49948:744934b818c7 user:haftmann date:Sat Oct 20 09:12:16 2012 +0200 summary: moved quite generic material from theory Enum to more appropriate places I can't say for sure if this is a correct result of the bijection, but it fits approximately in the time interval from my last successful (fast) test of everything. It is indeed the above changeset, notably the two code_simp invocations here: http://isabelle.in.tum.de/repos/isabelle/rev/744934b818c7#l9.7 This matches by offline analysis. As a first step, cf. the following changeset: http://isabelle.in.tum.de/reports/Isabelle/rev/8b50286c36d3 Testing this verson manually gives me 0:25:05 elapsed time total, while it is normally 0:16:30 on this machine with 8 cores and "build -j4 -a". In fact, one of the advantages of manual testing is that you immediately suffer from the effect yourself if something is wrong. I am busy elsewhere (in Orleans) the coming days ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs slow
On Mon, 22 Oct 2012, Florian Haftmann wrote: HOL-Proofs has become very slow, see http://www4.in.tum.de/~wenzelm/test/stats/mac-poly64-M8/HOL-Proofs.png Btw. how do those graphs come into being? The still official devel snapshot page does not link there… It is the normal output of Admin/isatest/isatest-stats. I am eating these charts for breakfast since > 5 years. For historical reasons, isatest does not publish these results when there is a failure, so it has to be done manually. (This detail can probably now be changed, since "the" development snapshot that accompanies a successful isatest run has lost its purpose.) These isatest statistics have proven to be essential to keep system performance in a reasonable range. So it is important to accumulated results continuously, even if they are not published on the spot. My usual complaints about isatest not working for more than 2-3 days are motivated by the effect of becoming "blind" wrt. these performance measurements. The Admin/isatest/settings are also carefully chosen (wrt. hardware, Poly/ML versions and options) such that certain aspects are measured, although this is far from exhaustive. It is one of the traditional shortcomings of mira/testboard, that systematic measurement and statistics are missing. Just this spring I ignored temporary "isatest blindness" before the Isabelle2012 release, with dire effects on the outcome (odd behaviour concerning signals masks and nohup). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs slow
> In such cases, the general question is if making the sources "canonical" > has any purpose. It is rather old material by Stefan Berghofer, written > in the typical style from around 2000, and not going to be revisited in > the foreseeable future. It is, as part of the story Spec_Rules vs. code default attribute. 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] HOL-Proofs slow
On Mon, 22 Oct 2012, Florian Haftmann wrote: I first thought it would be related to 1167c1157a5b (haftmann on src/Pure/Proof/extraction.ML), which is not immediately easy to follow in every detail. It indeed isn't, but the effect is idempotent. To my defence, reordering arguments is not very comprehensible from a diff. In such cases, the general question is if making the sources "canonical" has any purpose. It is rather old material by Stefan Berghofer, written in the typical style from around 2000, and not going to be revisited in the foreseeable future. There are no fundamental known problems with it. So why change it in the first place? Concerning the digestability of the changeset, it did not turn out as bad as first anticipated. Bitbucket has pretty good word-wise diffs. So after spending about 45min with: https://bitbucket.org/makarius/isabelle/changeset/1167c1157a5b83b05bd259adb7ee9b7729d98303 I came to the conclusion that the changeset is clean. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Proofs slow
> I first thought it would be related to 1167c1157a5b (haftmann on > src/Pure/Proof/extraction.ML), which is not immediately easy to follow > in every detail. It indeed isn't, but the effect is idempotent. To my defence, reordering arguments is not very comprehensible from a diff. 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] HOL-Proofs slow
>> Bijection then produced this: >> >> The first bad revision is: >> changeset: 49948:744934b818c7 >> user:haftmann >> date:Sat Oct 20 09:12:16 2012 +0200 >> summary: moved quite generic material from theory Enum to more >> appropriate places >> >> >> I can't say for sure if this is a correct result of the bijection, but >> it fits approximately in the time interval from my last successful >> (fast) test of everything. > > It is indeed the above changeset, notably the two code_simp invocations > here: > > http://isabelle.in.tum.de/repos/isabelle/rev/744934b818c7#l9.7 This matches by offline analysis. As a first step, cf. the following changeset: > http://isabelle.in.tum.de/reports/Isabelle/rev/8b50286c36d3 With this I get the following quite reasonable figures > Building HOL ... > Finished HOL (0:02:51 elapsed time, 0:05:14 cpu time, factor 1.83) > Building HOL-Main ... > Finished HOL-Main (0:02:03 elapsed time, 0:03:41 cpu time, factor 1.79) > Building HOL-Plain ... > Finished HOL-Plain (0:00:44 elapsed time, 0:01:15 cpu time, factor 1.70) > Building HOL-Proofs ... > Finished HOL-Proofs (0:07:52 elapsed time, 0:14:12 cpu time, factor 1.80) but we should avoid isatest measurements first. Nevertheless I have been thinking about rephrasing these proofs anyway, let's see. > HOL-Proofs has become very slow, see > http://www4.in.tum.de/~wenzelm/test/stats/mac-poly64-M8/HOL-Proofs.png Btw. how do those graphs come into being? The still official devel snapshot page does not link there… Cheers, 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] HOL-Proofs slow
On Sun, 21 Oct 2012, Makarius wrote: Bijection then produced this: The first bad revision is: changeset: 49948:744934b818c7 user:haftmann date:Sat Oct 20 09:12:16 2012 +0200 summary: moved quite generic material from theory Enum to more appropriate places I can't say for sure if this is a correct result of the bijection, but it fits approximately in the time interval from my last successful (fast) test of everything. It is indeed the above changeset, notably the two code_simp invocations here: http://isabelle.in.tum.de/repos/isabelle/rev/744934b818c7#l9.7 Is there a way to bypass that in Main HOL? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] HOL-Proofs slow
HOL-Proofs has become very slow, see http://www4.in.tum.de/~wenzelm/test/stats/mac-poly64-M8/HOL-Proofs.png I first thought it would be related to 1167c1157a5b (haftmann on src/Pure/Proof/extraction.ML), which is not immediately easy to follow in every detail. Bijection then produced this: The first bad revision is: changeset: 49948:744934b818c7 user:haftmann date:Sat Oct 20 09:12:16 2012 +0200 summary: moved quite generic material from theory Enum to more appropriate places I can't say for sure if this is a correct result of the bijection, but it fits approximately in the time interval from my last successful (fast) test of everything. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
