Email Gateway (Aug 23 2022 at 08:47): Email Gateway (Aug 23 2022 at 08:47):From: Tobias Nipkow <nipkow@in.tum.de>
On 21/04/2020 18:23, Makarius wrote:
So how about a reform like this:
* Other library sessions that are not sufficiently strong to stand on their
own feet (e.g. as AFP entry) are merged into HOL-Library. HOL-Analysis remains
separate; maybe also HOL-Number_Theory and similar sessions.
I would not bloat Library further by merging established sessions with it. (*)
* Theory HOL-Library.Library is discontinued. Historically it started out as
counterpart to theory "Main" in session "HOL", but later many HOL-Library
theories were excluded due to type-class instance conflicts. Thus its
secondary use as all-inclusive test theory for Isabelle/PIDE has become
obsolete and misleading: it misses too many theories. (PIDE could provide
other means to load all theories of a session.)
Yes!
* It becomes common practice to include example theories into the
HOL-Library session --- as leafs in the import graph, to avoid slow-down of
reloading the core HOL-Library theories in applications. Example: theory
HOL-ex.SOS becomes HOL-Library.Sum_of_Squares_Examples.
See (*)
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 08:59):From: Lawrence Paulson <lp15@cam.ac.uk>
There are more than 140 entries in HOL-Library, 97 of which are imported directly by Library.thy, and perhaps it’s worth discussing whether the library should be split up in some way. Some of the entries are miscellaneous small developments, while others are more specialised, e.g. setting up overloading in a particular way, or setting up code generation for particular types.
Larry
Email Gateway (Aug 23 2022 at 09:00):From: Manuel Eberl <eberlm@in.tum.de>
In my understanding, you're not supposed to import HOL-Library.Library
directly anyway, nor are you supposed to build on HOL-Library as a
parent session.
The only possible reason that I can imagine to split up HOL-Library
would be to make it easier to find things in it or get an overview of
what is there. Like a "HOL-Library for lists", "HOL-Library for
mathematics", "HOL-Library for tooling (such as records, code
generation, etc.)".
That might be make sense. Of course, one would have to go through it all
and determine a sensible categorisation first.
Manuel
Email Gateway (Aug 23 2022 at 09:00):From: Makarius <makarius@sketis.net>
On 21/04/2020 11:39, Manuel Eberl wrote:
In my understanding, you're not supposed to import HOL-Library.Library
directly anyway, nor are you supposed to build on HOL-Library as a
parent session.
Yes, de-facto this has become common practice in recent years: instead of
building on bulky session images, you merely import individual theories from
other sessions.
Now that the "session-qualified theory name" reform is full pushed through,
this should work smoothly.
The only possible reason that I can imagine to split up HOL-Library
would be to make it easier to find things in it or get an overview of
what is there. Like a "HOL-Library for lists", "HOL-Library for
mathematics", "HOL-Library for tooling (such as records, code
generation, etc.)".That might be make sense. Of course, one would have to go through it all
and determine a sensible categorisation first.
Such an organization around concepts has happened with
HOL-Computational_Algebra, HOL-Number_Theory etc.
But how should this scale to really big and complex libraries with many stages
and interdependencies? A session tree is rather inflexible for categorisation
of things.
It might be better to have just a few non-specific libraries, and some formal
tagging to say which to which "topic" a theory (or section within a theory)
belongs to. E.g. "algebra", "analysis", "number_theory" as formal annotations
instead of session directories.
Makarius
Email Gateway (Aug 23 2022 at 09:00):From: Tobias Nipkow <nipkow@in.tum.de>
Library/ improvements:
more tags/comments (together with better search engines (eg the work at
Cambridge and Fabian Huch's work))
stylized file names (eg Code_, List_)
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 09:00):From: Manuel Eberl <eberlm@in.tum.de>
Speaking of which, I just noticed that HOL-Computational_Algebra builds
on HOL-Library as a parent session. Is this really a good idea?
Manuel
Email Gateway (Aug 23 2022 at 09:00):From: Makarius <makarius@sketis.net>
be merged with HOL-Library.
Maybe we should step even further back and reconsider the overall
understanding of HOL-Library to reform it. Many years ago, I introduced it as
a supplement to Main HOL, in order to collect lots of material while keeping
the HOL image reasonably small. A lot has happened in the meantime.
So how about a reform like this:
* The session image HOL-Library should be rarely used as a parent in
applications. Instead it becomes an import session ('sessions' in ROOT) and
its theories are loaded again in the application (this retains original names
like HOL-Library.BigO).
* Other library sessions that are not sufficiently strong to stand on their
own feet (e.g. as AFP entry) are merged into HOL-Library. HOL-Analysis remains
separate; maybe also HOL-Number_Theory and similar sessions.
* Theory HOL-Library.Library is discontinued. Historically it started out as
counterpart to theory "Main" in session "HOL", but later many HOL-Library
theories were excluded due to type-class instance conflicts. Thus its
secondary use as all-inclusive test theory for Isabelle/PIDE has become
obsolete and misleading: it misses too many theories. (PIDE could provide
other means to load all theories of a session.)
* It becomes common practice to include example theories into the
HOL-Library session --- as leafs in the import graph, to avoid slow-down of
reloading the core HOL-Library theories in applications. Example: theory
HOL-ex.SOS becomes HOL-Library.Sum_of_Squares_Examples.
* Session HOL-Library is renamed to Library to simplify references without
quotes. When session-qualified names become part of the internal name space,
that will be also relevant for proper identifiers like "Library.BigO.bigo"
(quotes don't work inside the term language).
Anything else?
Makarius
Last updated: Apr 20 2024 at 04:19 UTC