Hi Thomas _Sewell_, no no don't worry, the report was from Thomas _Tuerk_! And the change was not too hard to produce.
What were your problems with the let-simproc? Did it to much or not enough unfolding? - Johannes Am Donnerstag, den 07.02.2013, 11:34 +1100 schrieb Thomas Sewell: > I'd forgotten I'd ever reported this to you. > > My problems with let_simproc run a little deeper anyway, and I've moved > to a different approach in the meanwhile. Sorry if I've left you > labouring on my behalf. > > Yours, > Thomas. > > On 07/02/13 02:38, Johannes Hölzl wrote: > > Am Mittwoch, den 06.02.2013, 12:25 +0100 schrieb Makarius: > >> On Tue, 5 Feb 2013, Johannes Hölzl wrote: > >> > >>> there is a bugproblem with the let-simproc, resulting in a non > >>> terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of > >>> isabelle-release): > >>> > >>> theory Scratch imports Complex_Main begin > >>> > >>> lemma "(let x = Collect P in R x x ∧ (Ball s P)) = X" > >>> using [[simp_trace]] > >>> apply simp > >>> > >>> The attached hg-bundle changes this behaviour to a terminating simproc. > >>> (The bundle can be applied to a repo containing #58e2d0cd81ae by > >>> "hg pull let_simp_betaeta.bundle") > >>> > >>> It currently runs in the testboard: > >>> http://isabelle.in.tum.de/testboard/Isabelle/rev/31f3b7c70a2c > >>> > >>> @Makarius: Is it possible to include this patch in Isabelle2013, when > >>> the testboard run is green? > >> Testboard does not test very much, compared to what has been tested > >> manually and semi-automatically in the past 2 weeks for the release. AFP > >> would also have to be covered. > >> > >> Anyway, this behaviour of let_simproc seems to have been there from its > >> beginning, or at least back until Isabelle2011 (what is what I have > >> tried). Nobody has noticed a problem in several years, so this change is > >> for the next release, unless there are really strong reasons to revisit it > >> now. > >> > >> > >> Makarius > > Thomas reported the problem to me. For me it is okay to fix it after > > Isabelle2013. > > > > @Thomas: Is it important for you to fix it in Isabelle2013? I hope the > > workaround with adding Let_def to the simplifier should work fine. Then > > I will add it just to the development version of Isabelle. > > > > - Johannes > > > > > > > > > > > > _______________________________________________ > > isabelle-dev mailing list > > [email protected] > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
