[isabelle-dev] HOL/Library/BigO.thy

[Makarius]

On 11/01/2023 09:06, Tobias Nipkow wrote:
> 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.

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