Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Naming policy of sessions in the AFP

view this post on Zulip Email Gateway (Sep 29 2021 at 10:20):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

the following sessions in the AFP

have in common that they

a) define more than one session;
b) at least one session bears a name that does not resemble the
directory name

and for some of them also holds that

c) the session from b) is used in sessions which reside in another
(toplevel) directory.

E. g. session JNF-AFP-Lib defined in Polynomial_Factorization but used
in Jordan_Normal_Form.

With increasing complexity, that complicates typical maintenance tasks
in the AFP.

What a brush-up be worth the effort?

Florian
OpenPGP_signature

view this post on Zulip Email Gateway (Sep 29 2021 at 10:31):

From: Makarius <makarius@sketis.net>
This one looks like a development artifact. The description says "Theories
from HOL-Library and the Archive of Formal Proofs that are used by this entry".

Often such statements become false later on, e.g. here it is used by another
entry also, and nobody can say for sure which theories are really required.

We already have options like "isabelle jedit -R ..." to let Isabelle work out
the dependencies and build an auxiliary image.

So JNF-AFP-Lib looks like a candidate for deletion.

Makarius

view this post on Zulip Email Gateway (Sep 29 2021 at 23:18):

From: Gerwin Klein <kleing@unsw.edu.au>
As Makarius says, some of this might have been for development reasons, possibly predating Isabelle features that make the split obsolete.

I would suggest consulting the authors of these entries before going ahead with reorganisation, though. They are all available with contact information in the metadata file.

Cheers,
Gerwin
signature.asc

view this post on Zulip Email Gateway (Sep 30 2021 at 07:09):

From: Tobias Nipkow <nipkow@in.tum.de>
On 30/09/2021 01:17, Gerwin Klein wrote:

As Makarius says, some of this might have been for development reasons, possibly predating Isabelle features that make the split obsolete.

I would suggest consulting the authors of these entries before going ahead with reorganisation, though. They are all available with contact information in the metadata file.

Absolutely!

Tobias

Cheers,
Gerwin

On 29 Sep 2021, at 20:19, Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de> wrote:

Hi all,

the following sessions in the AFP

have in common that they

a) define more than one session;
b) at least one session bears a name that does not resemble the
directory name

and for some of them also holds that

c) the session from b) is used in sessions which reside in another
(toplevel) directory.

E. g. session JNF-AFP-Lib defined in Polynomial_Factorization but used
in Jordan_Normal_Form.

With increasing complexity, that complicates typical maintenance tasks
in the AFP.

What a brush-up be worth the effort?

Florian

smime.p7s

view this post on Zulip Email Gateway (Sep 30 2021 at 10:22):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Hi all,

for the entries Berlekamp_Zassenhaus and Polynomial_Factorization, I will (try to) remove the auxiliary sessions.

Best,
René

Last updated: Jan 04 2025 at 20:18 UTC