[isabelle-dev] Broken AFP sessions

[Larry Paulson]

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 <traytel at inf.ethz.ch> 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 <makarius at sketis.net> 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-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev