Re: [isabelle-dev] buildall inconsistency

[Jose Divasón]

Dear all,

Thanks Manuel for your changes about euclidean rings!

Jesús Aransay and I are now introducing a few changes in the Echelon_Form
development. In addition, we are also polishing the code. We hope to finish
it in the following days.

Cheers,
Jose


2016-02-28 21:29 GMT+01:00 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 mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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