Stream: math-comp users

Topic: MathComp LOC


view this post on Zulip Karl Palmskog (Jun 10 2023 at 12:58):

I was a bit sad to see MathComp missing here:
mathlibs.jpeg

from this tweet.

However, this may be due to unavailability of up-to-date statistics for (1) the math-comp repo code and (2) all projects in the mathcomp logical path? For marketing reasons, one may want to compute this regularly.

view this post on Zulip Théo Zimmermann (Jun 12 2023 at 07:26):

agda-stdlib is present in this list but the coq-stdlib is missing. And yet, it is trivial to compute its LoC count.

view this post on Zulip Karl Palmskog (Jun 12 2023 at 08:50):

sure, but is the Coq Stdlib even claiming to be a mathematical library at this point? I feel it's more of a general utility library, so not as obvious it should be in the list.

view this post on Zulip Théo Zimmermann (Jun 12 2023 at 10:56):

Does agda-stdlib claims to be a mathematical library?

view this post on Zulip Karl Palmskog (Jun 12 2023 at 10:59):

I think the reason Agda-stdlib was included here is because this was from the author of Agda-unimath, and if I remember correctly Agda-stdlib is only big standalone library for Agda (besides Agda-unimath)

view this post on Zulip Théo Zimmermann (Jun 12 2023 at 11:01):

Sure, I just meant that this list is random and far from exhaustive or consistent (whatever criterion we choose).


Last updated: Jul 15 2024 at 21:02 UTC