eberlm at in.tum.de
Tue Apr 9 15:32:11 CEST 2019
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.
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
>> 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
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev