Karl Palmskog (Jun 06 2022 at 17:04): 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
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:
- probability
- machine words
- classical analysis
- finite sets and maps
... 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.
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
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?
Bas Spitters (Jun 06 2022 at 17:48):Sounds like Coq universe could be relevant for this ??
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
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
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
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
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.
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
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: Apr 20 2024 at 12:02 UTC