[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 <eberlm at in.tum.de>:

> 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 <eberlm at in.tum.de> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160301/be3240d5/attachment.html>