[isabelle-dev] Broken AFP

[Manuel Eberl]

Hallo,

sorry for the broken AFP – it's my fault, but I added a lot of new 
material about rings and prime factor decomposition. The projects that 
were affected by this the most are already fixed, and I will take care 
of the rest on Monday.


Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Broken AFP sessions

[Dmitriy Traytel]

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

Re: [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  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

[Makarius]

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

[isabelle-dev] Broken AFP sessions

[Makarius]

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