Re: [isabelle-dev] HOL-Algebra

[Florian Haftmann]

Hi all,

just a few comments on my behalf.

>> We’ve decided that Group-Ring-Module is irremediable, and are using it
>> only as a list of useful results that need to be done again.

Seems to make sense.

> Just one oddity in HOL-Algebra: It claims canonical theory names like> 
> "Group", "Ring", "Module". Thus the main HOL session needs to evade
via> non-standard names "Groups", "Rings", "Modules" (the latter is new
in> 2af1f142f855).

This pragmatic tradition had been started by »Orderings.thy«; I'm
uncertain whether it is worth the effort to change it.

Note that the theories »More_*.thy« contain material contributed by
Jeremy Avigad but not situated in HOL-Algebra in the first place; when
collecting this I did not want to touch the original theories, but as
part of a rework those theories could be integrated.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] HOL-Algebra

[Makarius]

On 12/05/18 11:40, Lawrence Paulson wrote:
> I’m talking about HOL-Algebra, and as I’ve seen myself, parts of it are
> ancient. They desperately need updating and streamlining.
> 
> We’ve decided that Group-Ring-Module is irremediable, and are using it
> only as a list of useful results that need to be done again.

Just one oddity in HOL-Algebra: It claims canonical theory names like
"Group", "Ring", "Module". Thus the main HOL session needs to evade via
non-standard names "Groups", "Rings", "Modules" (the latter is new in
2af1f142f855).


Just for theory names, we now have session-qualifiers, i.e. HOL.Group
vs. HOL-Algebra.Group would work, but the internal name spaces are not
qualified separately, and a merge does not work.

At some point, I would like to see the long theory name also as internal
name space qualifier, e.g. "HOL-Algebra.Group", but there are some
remaining problems:

  * It needs to be implemented properly, in particular for tools that
pretend to know Isabelle name space policies (by analyzing the structure
of full names).

  * Non-identifiers as session names are bad, e.g. a constant name
HOL-Algebra.Group.group cannot be used within a term. We would have to
rename many sessions. This is particularly difficult in AFP, where
session names and entry names (with resulting URLs) should usually coincide.


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

Re: [isabelle-dev] HOL-Algebra

[Lawrence Paulson]

I’m talking about HOL-Algebra, and as I’ve seen myself, parts of it are 
ancient. They desperately need updating and streamlining.

We’ve decided that Group-Ring-Module is irremediable, and are using it only as 
a list of useful results that need to be done again.

Larry

> On 11 May 2018, at 23:40, Makarius  wrote:
> 
> Is the chaotic naming in Group-Ring-Module or HOL-Algebra? According to
> my information, Clemens Ballarin has taken great care about HOL-Algebra
> over many years (even with contributions by students).
> 

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

Re: [isabelle-dev] HOL-Algebra

[Makarius]

On 08/05/18 13:49, Lawrence Paulson wrote:
> I have two interns from École Polytechnique. They have been going over 
> HOL-Algebra and Group-Ring-Module, providing new proofs of the best results 
> in the latter and tidying up some messy proofs in the former, as well. They 
> are also systematising the chaotic naming conventions that they found there. 
> So there will be big changes to HOL-Algebra in the coming weeks. This is an 
> early warning in case anybody else wants to work on this directory.

Is the chaotic naming in Group-Ring-Module or HOL-Algebra? According to
my information, Clemens Ballarin has taken great care about HOL-Algebra
over many years (even with contributions by students).

Beyond that, I am just hoping that we are not sliding into the "best
practices" of the average Github project, with huge commits / merges
coming out of the blue, which are hard to understand later.

Both the sources and their history need to be readable, in order to sort
out subtle problems. These days I read history even more often than the
latest version of the sources.


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

Re: [isabelle-dev] HOL-Algebra

[Manuel Eberl]

I have a student who was going to formalise things about fields and
field extensions. Does that clash with your work in any way?

In any case, we should definitely coordinate our efforts here to avoid
duplication of work.

Manuel


On 2018-05-08 13:49, Lawrence Paulson wrote:
> I have two interns from École Polytechnique. They have been going over 
> HOL-Algebra and Group-Ring-Module, providing new proofs of the best results 
> in the latter and tidying up some messy proofs in the former, as well. They 
> are also systematising the chaotic naming conventions that they found there. 
> So there will be big changes to HOL-Algebra in the coming weeks. This is an 
> early warning in case anybody else wants to work on this directory.
>
> Larry
>
> ___
> 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] HOL-Algebra

[Lawrence Paulson]

I have two interns from École Polytechnique. They have been going over 
HOL-Algebra and Group-Ring-Module, providing new proofs of the best results in 
the latter and tidying up some messy proofs in the former, as well. They are 
also systematising the chaotic naming conventions that they found there. So 
there will be big changes to HOL-Algebra in the coming weeks. This is an early 
warning in case anybody else wants to work on this directory.

Larry

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