Re: [isabelle-dev] Broken AFP sessions
On Wed, 7 Oct 2015, Larry Paulson wrote: Now I’ve fixed these too. Great. So in Isabelle/a273bdac0934 and AFP/2351d0b91fb8 everything works, except for the new entry Isabelle_Meta_Model from Isabelle2015. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Broken AFP sessions
It’s a bit mysterious. On Monday I got a failure message from the AFP and checked the status page. Four entries were shown as not working. I’ve tried them on my own machine (no matter precisely which version of the sources I had, it certainly had that simprule change, which I had made myself) and three of the four ran perfectly. I fixed the fourth one by adding the obvious simp del: real_of_nat_Suc and that should have been that. Now I’ve fixed these too. Larry > On 7 Oct 2015, at 08:33, Dmitriy Traytel wrote: > > Those look to me as if they have to do with 2314c2f62eb1 (real_of_nat_Suc is > now a simprule). Verified only for the Integral.thy failure. > > Dmitriy > > >> On 06 Oct 2015, at 23:19, Makarius wrote: >> >> Here are some more proof failures (Isabelle/5b5656a63bd6 and >> AFP/21bdf9fbf229): >> >> Integration FAILED >> *** At command "by" (line 1724 of >> "~/isabelle/afp-devel/thys/Integration/Integral.thy") >> >> Markov_Models FAILED >> *** At command "done" (line 1038 of >> "~/isabelle/afp-devel/thys/Markov_Models/Classifying_Markov_Chain_States.thy") >> *** At command "by" (line 1077 of >> "~/isabelle/afp-devel/thys/Markov_Models/Classifying_Markov_Chain_States.thy") >> >> Ordinary_Differential_Equations FAILED >> *** At command "by" (line 804 of >> "~/isabelle/afp-devel/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy") >> *** At command "by" (line 704 of >> "~/isabelle/afp-devel/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy") >> >> >> 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 mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Broken AFP sessions
Those look to me as if they have to do with 2314c2f62eb1 (real_of_nat_Suc is now a simprule). Verified only for the Integral.thy failure. Dmitriy > On 06 Oct 2015, at 23:19, Makarius wrote: > > Here are some more proof failures (Isabelle/5b5656a63bd6 and > AFP/21bdf9fbf229): > > Integration FAILED > *** At command "by" (line 1724 of > "~/isabelle/afp-devel/thys/Integration/Integral.thy") > > Markov_Models FAILED > *** At command "done" (line 1038 of > "~/isabelle/afp-devel/thys/Markov_Models/Classifying_Markov_Chain_States.thy") > *** At command "by" (line 1077 of > "~/isabelle/afp-devel/thys/Markov_Models/Classifying_Markov_Chain_States.thy") > > Ordinary_Differential_Equations FAILED > *** At command "by" (line 804 of > "~/isabelle/afp-devel/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy") > *** At command "by" (line 704 of > "~/isabelle/afp-devel/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy") > > > 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] Broken AFP sessions
Here are some more proof failures (Isabelle/5b5656a63bd6 and AFP/21bdf9fbf229): Integration FAILED *** At command "by" (line 1724 of "~/isabelle/afp-devel/thys/Integration/Integral.thy") Markov_Models FAILED *** At command "done" (line 1038 of "~/isabelle/afp-devel/thys/Markov_Models/Classifying_Markov_Chain_States.thy") *** At command "by" (line 1077 of "~/isabelle/afp-devel/thys/Markov_Models/Classifying_Markov_Chain_States.thy") Ordinary_Differential_Equations FAILED *** At command "by" (line 804 of "~/isabelle/afp-devel/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy") *** At command "by" (line 704 of "~/isabelle/afp-devel/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy") Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev