[isabelle-dev] Homology

[Makarius]

On 09/04/2019 14:06, Manuel Eberl wrote:
> Importing Algebra sounds like it would come with various unforeseen
> consequences.
> 
> The more modular approach seems more workable to me. I for one think
> that there's no rush; I'd wait until the next release cycle.

I won't participate in this particular discussion about HOL-Algebra vs.
HOL-Analysis, because I don't know much about its internal structure and
applications on top of it.


Just a general note for post-Isabelle2019, or post-post-Isabelle2019.
The more the libraries are growing, the less it is clear how to make a
hierarchy according to topics (like "Algebra", "Analysis",
"Number_Theory" etc.): there will be complexities in the dependencies
that might force to introduce Algebra1, Analysis1, Algebra2, Analysis2 etc.

So in the worst case there is a trend towards more diverse (or
amorphic?) library sessions. HOL-Analysis itself already shows such
tendencies.

Since some libraries are advertized as "batteries included", one could
also try to organize things according to which batteries (very small to
very large), e.g.

   AAAA Main
   AAA Complex_Main
   AA Algebra, basic Analysis
   C full Analysis with Homology etc.
   D HOL-ODE etc.

For the funny letters see https://en.wikipedia.org/wiki/AAA_battery --
it merely illustrates the idea, and is not meant literally.


	Makarius