[isabelle-dev] Homology

[Manuel Eberl]

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190409/86bf3494/attachment-0002.html>