Re: [isabelle-dev] Fwd: isabelle test failed
On Fri, 26 Jun 2015, Larry Paulson wrote: HOL-Proofs, etc., have been failing for several days now. Last time I checked, it was simply a timeout. Presumably some change to rewriting is to blame. It may be similar to the AFP failure that I fixed yesterday. Is anyone familiar with this entry? I've made some manual tests just yesterday and then produced the following change: changeset: 60574:915da29bf5d9 user:wenzelm date:Thu Jun 25 22:56:33 2015 +0200 files: Admin/isatest/settings/at64-poly description: more heap -- hoping for more stability of HOL-Proofs; The isatest from tonight did not see that yet, because I pushed it too late after midnight. Maybe the next test run works. The deeper reason why HOL-Proofs takes much longer now is this: The first bad revision is: changeset: 60046:894d6d863823 user:traytel date:Mon Apr 13 13:03:41 2015 +0200 summary: call Goal.prove only once for a quadratic number of theorems I did not find time yet, to look more closely what is behind that. Generally, proof term performance is bad for massive amounts of goals with Pure.conjunction. I've had a discussion about that around 2008 with Stefan Berghofer, but he could not explain it, nor improve the situation. More generally, HOL-Proofs always serves as a reminder of invisible concrete walls concerning limited CPU resources. Growth cannot just continue forever, one day it will come to a grinding halt. (Despite that triviality, I have already some ideas to reduce resource usage once again, so that the meltdown might be postponed.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: isabelle test failed
Oops, I didn't expect my name to appear here ;-) The changeset 894d6d863823 was a reaction to Andreas Lochbihler's report [1]. With turned off proofs the effect was a good one. What is special about Pure.conjunction w.r.t. proof reconstruction? Is it something in Goal.conjunction_tac? Would you advise to use HOL's conjunction instead? Dmitriy [1] https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-April/005986.html On 26.06.2015 20:01, Makarius wrote: On Fri, 26 Jun 2015, Larry Paulson wrote: HOL-Proofs, etc., have been failing for several days now. Last time I checked, it was simply a timeout. Presumably some change to rewriting is to blame. It may be similar to the AFP failure that I fixed yesterday. Is anyone familiar with this entry? I've made some manual tests just yesterday and then produced the following change: changeset: 60574:915da29bf5d9 user:wenzelm date:Thu Jun 25 22:56:33 2015 +0200 files: Admin/isatest/settings/at64-poly description: more heap -- hoping for more stability of HOL-Proofs; The isatest from tonight did not see that yet, because I pushed it too late after midnight. Maybe the next test run works. The deeper reason why HOL-Proofs takes much longer now is this: The first bad revision is: changeset: 60046:894d6d863823 user:traytel date:Mon Apr 13 13:03:41 2015 +0200 summary: call Goal.prove only once for a quadratic number of theorems I did not find time yet, to look more closely what is behind that. Generally, proof term performance is bad for massive amounts of goals with Pure.conjunction. I've had a discussion about that around 2008 with Stefan Berghofer, but he could not explain it, nor improve the situation. More generally, HOL-Proofs always serves as a reminder of invisible concrete walls concerning limited CPU resources. Growth cannot just continue forever, one day it will come to a grinding halt. (Despite that triviality, I have already some ideas to reduce resource usage once again, so that the meltdown might be postponed.) 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
[isabelle-dev] NEWS: cases from goals
* Proof method goals turns the current subgoals into cases within the context; the conclusion is bound to variable ?case in each case. * The undocumented feature of implicit cases goal1, goal2, goal3, etc. is marked as legacy, and will be removed eventually. Note that proof method goals achieves a similar effect within regular Isar. This refers to c708dafe2220 and d2fbc021a44d. Example updates of oldd proofs are can be seen in changeset 7e741e22d7fc. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: structured Isar goal statements (update)
On Wed, 24 Jun 2015, Makarius wrote: The keyword 'when' may be used instead of 'if', to indicate 'presume' instead of 'assume' above. This refers to Isabelle/51a6997b1384. The 'presume' element is rarely used, and the 'when' eigen-context is mainly an exercise in orthogonality of the language. There might be useful applications nonetheless, e.g. see the examples about suffices-to-show in ~~/src/HOL/Isar_Examples/Structured_Statements.thy Now that 'presume' semantics has a separate syntax, the normal == is free to be re-interpreted. So here is another breaking NEWS entry for Isabelle/804dfdc82835: * The meaning of 'show' with Pure rule statements has changed: premises are treated in the sense of 'assume', instead of 'presume'. This means, a goal like ⋀x. A x ⟹ B x ⟹ C x can be solved completely as follows: show ⋀x. A x ⟹ B x ⟹ C x or: show C x if A x B x for x Rare INCOMPATIBILITY, the old behaviour may be recovered as follows: show C x when A x B x for x This means the common beginner-mistake to use Pure rule statements for show no longer leads to bad surprises. As a consequence, there might be more ugly proofs emerging than necessary, but better than no proof at all in the first attempt. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: isabelle test failed
On Sat, 27 Jun 2015, Dmitriy Traytel wrote: Oops, I didn't expect my name to appear here ;-) The changeset 894d6d863823 was a reaction to Andreas Lochbihler's report [1]. With turned off proofs the effect was a good one. What is special about Pure.conjunction w.r.t. proof reconstruction? Is it something in Goal.conjunction_tac? Would you advise to use HOL's conjunction instead? I don't know if there is a difference between Pure and HOL. We could ask Stefan Berghofer, or just check empirically. The question arose first in 2007/2008 when Alex Krauss introduced many multi-goals in the function package. I can't say on the spot if/how that was addressed, or rather worked-around. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: cases from goals
Multivariate_Analysis/Integration.thy uses goal1 206 times, so this will take a while. Larry On 26 Jun 2015, at 23:46, Makarius makar...@sketis.net wrote: * Proof method goals turns the current subgoals into cases within the context; the conclusion is bound to variable ?case in each case. * The undocumented feature of implicit cases goal1, goal2, goal3, etc. is marked as legacy, and will be removed eventually. Note that proof method goals achieves a similar effect within regular Isar. This refers to c708dafe2220 and d2fbc021a44d. Example updates of oldd proofs are can be seen in changeset 7e741e22d7fc. 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
