I would try to avoid HOL-Algebra as much as possible. The entire library is not in a great state and introducing unnecessary dependencies on it should be avoided.
There is much work to be done there. Manuel On 09/04/2019 15:25, Makarius wrote: > 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 > >
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
