There are at least the following libraries on EC in Coq:

https://github.com/thery/EdwardsEllipticCurve

https://github.com/thery/coqprime by @Laurent Théry

https://github.com/strub/elliptic-curves-ssr by @Pierre-Yves Strub

and https://github.com/mit-plv/fiat-crypto by @Andres Erbsen and @Jason Gross , which uses Coq prime.

I understand the history of these libraries. I know @Andres Erbsen has been working on integrating libraries.

Are there any plans on how to use/develop these libraries in the future?

I see some of these libraries could be added to Awesome Coq...

CoqPrime and Fiat Crypto are in Awesome Coq and in the Coq Platform. I didn't add `elliptic-curves-ssr`

since unsure if maintained, and the Edwards one is likely new?

it's not obvious to me how one can group these other than by dependency on MathComp (elliptic-curves-ssr, Edwards)

My lib is in maintenance mode only

Having to running with the last version of mathcomp should be easy.

But there won't be any new results added (by me)

The Edwards one is from four years ago. It formalizes the elegant proof by Tom Hales.

is it really all that easy to port elliptic-curves-ssr to MC 2.0? For insiders maybe.

The difference between MC 1 and MC 2 is really in the use of Hierarchy-Builder for the structures. Apparently, elliptic-curve-ssr contains 4 structures and 173 instances so I'd expect the port to be relatively easy.

recall that our door is open for proposing to move/consolidate projects. We try to facilitate discussions with original authors for getting useful packages/code on track to releases and/or Platform. However, without a volunteer maintainer, a proposal likely won't get far.

Bas Spitters said:

There are at least the following libraries on EC in Coq:

....

https://github.com/thery/coqprime by Laurent Théry

....

just for completness I have also ported the elliptic curve of `coqprime`

in mathcomp here

Nice! I didn't know about math-comp-extra.

Is there a good overview of the math-comp ecosystem somewhere? Including information about what is hoped to be maintained in the longer run, CI, etc ? I looked here:

https://github.com/math-comp/math-comp

https://math-comp.github.io/

But didn't see it.

I see it's mentioned here. Maybe the MC libraries should also be grouped together (also search works OK).

https://github.com/coq-community/awesome-coq

MathComp Extra is listed in Awesome Coq. However, grouping by MathComp doesn't fit the format of Awesome lists, which are usually by domain. What I can do is consistently add "Mathematical Components" somewhere in the description for projects that are explicitly based on MathComp. There are also projects that have some *optional* MathComp support, such as Relation Algebra, Autosubst, and these are difficult to classify

as for maintained in the long run, I think there are now two ways a project can be considered this way:

- it's in the Coq Platform
- the maintainers say it will be maintained in the long run

I'd say it's very rare to get a statement like 2. from any project, so a list of such projects seems unfeasible.

So, maybe mathcomp extra should be in the extended edition of the platform (I forgot the name).

[ I have no immediate plans of using it myself. ]

my view: results of general MathComp interest from MathComp Extra and similar smaller projects could go into [Platform project] CoqEAL by request, example: https://github.com/coq-community/coqeal/pull/70

Results in CoqEAL can then in turn be considered for inclusion into "proper" MathComp projects in the `mathcomp`

logpath prefix, or MathComp itself.

the MathComp wiki might be one way to link/document some of the smaller projects: https://github.com/math-comp/math-comp/wiki

Makes sense. Is there a reason to choose coqeal in particular for this? I guess because it's already in platform?

yes, it's already in the Platform, but also, it's already a collection of "utility" results of sorts, rather than a completely focused package

also a Coq-community project, so there less of a chance of results getting stuck in limbo

Coqeal was developed in the formath project as an Effective Algebra Library. I guess it's OK to shift focus if that's what the maintainers want.

"algebra" is a big subject, arguably a lot of CS is logic + algebra

for example, this repo description in my view covers quite a lot:

developments in algebra [...], and optimized algorithms on MathComp data structures.

Last updated: Jul 25 2024 at 15:02 UTC