Re: [isabelle-dev] buildall inconsistency

[Manuel Eberl]

I just successfully built the entire distribution and the entire AFP. 
(Isabelle a3c7bd201da7 / AFP 6d199a5)


I also removed the rogue "Euclidean Ring" definition and orphaned 
instances in Echelon_Form, but I think that Echelon_Form, Hermite, 
Algebraic_Numbers and the related entries are in dire need of a major 
cleanup. Echelon_Form/Rings2 in particular contains a lot of interesting 
material.



Cheers,

Manuel


On 28/02/16 15:45, Lawrence Paulson wrote:

Looks like valuable work even if it caused some disruption.
Larry


On 28 Feb 2016, at 13:32, Manuel Eberl  wrote:

Yes, this has something to do with my ongoing changes to Euclidean Rings and 
related stuff. Everything in the distribution already works again and, as for 
the AFP, I'm on it.

I've removed all of the redundant facts in Euclidean_Algorithm and moved all 
the facts that are not specific to Euclidean Rings to semiring_gcd and 
ring_gcd. I also took care of the appropriate subclass instances and fixed code 
generation for Gcd/Lcm.

Most importantly, I also adapted all the AFP entries that use the polynomial 
GCD to work with the GCD from Euclidean_Algorithm instead of their own 
instances.

We should be able to move Euclidean_Algorithm out of Number_Theory and into the 
main HOL soon.




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

[isabelle-dev] Disabled Jenkins mails

[Lars Hupel]

Dear list,

I have temporarily disabled all mails from Jenkins. I hope to re-enable
them soon with less useless traffic. Apologies for the spam.

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