Stream: math-comp users

Topic: Utility library coordination


view this post on Zulip Karl Palmskog (Jun 06 2022 at 17:04):

to be honest, there is a need for working groups for doing basic coordination of development of severals kinds of libraries in Coq:

... since existing libraries are to a large extent incompatible and have no interoperation/translation. But to even get to that point, we could at least try to get the key ones added to the Coq Platform and work from there

view this post on Zulip Evgeniy Moiseenko (Jun 06 2022 at 17:25):

Karl Palmskog said:

to be honest, there is a need for working groups for doing basic coordination of development of severals kinds of libraries in Coq:

... since existing libraries are to a large extent incompatible and have no interoperation/translation. But to even get to that point, we could at least try to get the key ones added to the Coq Platform and work from there

+1

I have recently faced the same incompatibility problem regarding finsets library.
I will be happy to use in my project the nominal sets theory developed by @Arthur Azevedo de Amorim, but it is based on extructures library, while I use mathcomp-finmap library.
It would be really nice to unify the two.

view this post on Zulip Ali Caglayan (Jun 06 2022 at 17:42):

Regarding machine words, here is something that is called "mathcomp-word" https://github.com/jasmin-lang/coqword

view this post on Zulip Bas Spitters (Jun 06 2022 at 17:44):

@Karl Palmskog Perhaps we can start by having a document (wiki?) to describe the differences/trade-offs?

view this post on Zulip Bas Spitters (Jun 06 2022 at 17:48):

Sounds like Coq universe could be relevant for this ??

view this post on Zulip Karl Palmskog (Jun 06 2022 at 17:51):

@Bas Spitters we can use the Coq wiki, sure. But more directly, there are action points, like adding at least one Coq word library (and also SSProve?) to the Coq Platform. Ali mentions coqword, but there is also: https://github.com/mit-plv/bbv

view this post on Zulip Karl Palmskog (Jun 06 2022 at 17:52):

the Coq universe is a nice way to collect Coq libraries that build with Dune, but the libraries also need to be packaged and maintained

view this post on Zulip Karl Palmskog (Jun 06 2022 at 17:55):

and we don't need to aim for integration of libraries always, I think just having some basic interoperability is enough some of the time

view this post on Zulip Karl Palmskog (Jun 06 2022 at 18:04):

one idea to start with is to make some kind of Wikipedia style comparison chart (e.g., https://en.wikipedia.org/wiki/Proof_assistant#System_comparison) for utility libraries by area

view this post on Zulip Bas Spitters (Jun 06 2022 at 18:11):

@Karl Palmskog @Ali Caglayan Remember this discussion about coq words.
This is currently an issue for us for the coq hacspec backend. One possibility would be to use modules to axiomatize the various theories, and have the existing libraries as instances, but that's not perfect.

view this post on Zulip Bas Spitters (Jun 06 2022 at 18:14):

Issue for SSProve in platform. We're working on stabilizing things. This also depends on progress on the math-comp (extructures vs finmap) and coq word sides.
https://github.com/coq/platform/issues/177

view this post on Zulip Karl Palmskog (Jun 06 2022 at 18:16):

coincidentally, I just packaged 8.16+rc1, so now may be a good time to (begin to) test+package stuff on the opam archive as a part of the process of putting it in the Platform for the 8.16 release this fall


Last updated: Feb 08 2023 at 07:02 UTC