Email Gateway (Jan 10 2023 at 11:57): Email Gateway (Jan 10 2023 at 11:57):From: Lawrence Paulson <lp15@cam.ac.uk>
This theory is ancient and looks it. It’s also totally unused and probably obsolete. Shall we delete it?
Larry
Email Gateway (Jan 10 2023 at 12:14):From: Tobias Nipkow <nipkow@in.tum.de>
If the author Jeremy agrees, sure, HOL/Library is getting rather large anyway.
Tobias
smime.p7s
Email Gateway (Jan 10 2023 at 17:46):From: Makarius <makarius@sketis.net>
This may be answered by figuring out its uses in applications. notably AFP.
There is also a clone of it in src/HOL/Metis_Examples/Big_O.thy --- I use that
regularly to test Isabelle/PIDE/Sledgehammer + ATPs, just because it comes
early in the alphabet and contains some nontrivial things.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 10 2023 at 17:53):From: Makarius <makarius@sketis.net>
A few more considerations:
* We have lots of "rubbish examples", notably in HOL-ex. Traditionally we
never really deleted old things, but rather upgraded them to the continuously
changing system (and library). This is a distinctive strength of Isabelle.
Sometimes it is fun to meet contributors from decades ago, and show them their
ancient experiments.
* We have recently introduced HOL-Examples for "prominent" or "notable"
examples. Very little has happened so far to sort things out, i.e. to move
more material from HOL-ex to HOL-Examples.
* HOL-Library was originally meant as support for "prominent" or "notable"
applications. It might have grown a bit uneven in recent years, but I can't
tell for sure.
So the ultra-short answer to this thread might just be: move Big_O from
HOL-Library to HOL-ex.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 11 2023 at 08:00):From: Gerwin Klein <kleing@unsw.edu.au>
I like that idea.
Cheers,
Gerwin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 11 2023 at 08:06):From: Tobias Nipkow <nipkow@in.tum.de>
The distribution is meant to provide a curated set of theories. They are in
constant flux anyway. And if some theory is definitely outdated we should remove
it rather than keep it around and confuse users. For archeological purposes we
have mercurial.
Tobias
smime.p7s
Email Gateway (Jan 11 2023 at 10:55):From: Lawrence Paulson <lp15@cam.ac.uk>
I agree with Tobias. We are already very good at preserving our past, but it’s exasperating when novices stumble across legacy material and emulate that style. Fortunately, there is not a single use of BigO anywhere in the AFP. Let’s delete it altogether.
Larry
Email Gateway (Jan 11 2023 at 11:34):From: Makarius <makarius@sketis.net>
This model does not really fit the past 10-20 (or 30?) years of the distribution.
Curation requires a lot of time and rarely happens. It is difficult to decide
what is so outdated that it can be removed without causing problems in some
odd applications (especially outside AFP).
This is why we have "light spots" (e.g. HOL-Library and HOL-Examples) and
"dark spots" (e.g. HOL-ex) in the distribution.
As an excercise in curation, we could do further moving between HOL-Library /
HOL-Examples / HOL-ex.
Something that looks odd / old / outdated can always find its home in HOL-ex
or as a separate session. Someone who depends on it can easily redirect
imports, and proceed. This will save a lot of time for everyone.
I am usually on the front to remove things that are no longer required,
escpecially when they constantly get in the way of ongoing maintenance.
Old examples rarely get in the way.
(Side-remark: Old documentation is another topic that I hardly dare to touch.
The classic Tutorial is particularly odd, and it sometimes does get into the
way with its special tricks on ToyList.thy.)
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 11 2023 at 11:42):From: Makarius <makarius@sketis.net>
What do you intend to do with its clone in src/HOL/Metis_Examples ?
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 11 2023 at 11:48):From: Lawrence Paulson <lp15@cam.ac.uk>
That is an entirely different situation. It’s used as test data. Nobody will get confused or distracted by that.
Larry
Email Gateway (Jan 11 2023 at 13:09):From: Makarius <makarius@sketis.net>
I find it confusing to have a clone with its original lost in time and space.
If you want to avoid general user confusion, the traditional approach is to
move it into the "HOL-ex" bin.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 11 2023 at 16:04):From: Lawrence Paulson <lp15@cam.ac.uk>
Since we describe that directory as “miscellaneous examples”, anything we put there needs to be presentable, so the theory will require a bit of tidying up.
Larry
Last updated: Apr 28 2024 at 12:28 UTC