search

coq / platform

Multi platform setup for Coq, Coq libraries and tools
Creative Commons Zero v1.0 Universal
187 stars 49 forks source link

Add relation-algebra to Coq Platform #167

Closed anton-trunov closed 2 years ago

anton-trunov commented 2 years ago

A very useful library with great automation: https://github.com/damien-pous/relation-algebra. (/CC @damien-pous)

damien-pous commented 2 years ago

Thanks @anton-trunov for the invitation. I agree with the inclusion of relation-algebra in the Coq Platform in agreement to the Coq Platform charter, at the full level. (I plan to provide at least compatibility releases for each new version of Coq - I've just done the one for v8.14)

MSoegtropIMC commented 2 years ago

@damien-pous: thanks for the confirmation. If there are no technical issues, I will include it in the Coq Platform release planned end of this month.

MSoegtropIMC commented 2 years ago

@damien-pous : sorry I had too much other things to do for the previous release, but 2022.03 is still open, and I am considering it. One issue is that I can't find an opam package. Is there one? Of not do you need help with creating one?

damien-pous commented 2 years ago

Hi @MSoegtropIMC, there are opam packages for coq versions up-to 8.14, under the name coq-relation-algebra. I should probably do a version for coq 8.15, I did not have a look at it yet...

MSoegtropIMC commented 2 years ago

Sorry, silly me - I was searching in the opam tree, but with find . -f -iname "*relation*" rather than find . -d -iname "*relation*". I would appreciate an opam file for 8.15 (preferably until Wednesday), but I could also create it.

damien-pous commented 2 years ago

Just did a release for coq 8.15 (relation-algebra 1.7.7), pull request waiting on opam-coq-archive...

MSoegtropIMC commented 2 years ago

@damien-pous : one question: I prefer to publish a mostly compatible package pick for the latest Coq and the previous latest one (8.15 and 8.14), so that people can first update the package pick and then Coq in separate steps. I see that relation-algebra 1.7.7 is not compatible for 8.14. Is this really so (for a good reason) or is this just untested? I could also leave it away in the compatible 8.14 pick since the porting argument isn't relevant here, but I wanted to ask for your opinion on this.

damien-pous commented 2 years ago

Hi @MSoegtropIMC, I've just tested, and unfortunately 1.7.7 is not compatible with 8.14 : I rely on some OCaml function in the plugins whose type changed from coq 8.14 to coq 8.15...

MSoegtropIMC commented 2 years ago

OK, thanks! I will then leave away relation-algebra in the 8.14~2022.03 pick and include it only in the 8.15~2022.03 pick.

MSoegtropIMC commented 2 years ago

@damien-pous : a note on our "smoke test kit" (a quick check Coq Platform does to check if all packages are installed properly): I selected the files compiler_opts.v and imp.v for smoke testing which appear to be examples and coqc reasonably fast. I would appreciate if in a future release you could change these files such that they use From RelationAlgebra Require ... to require modules from you package (you can link this to . in your _CoqProject file). As is I need to patch the files for smoke testing. This would be also useful for users trying your examples, because as is they won't run with an opam installed coq-relation-algebra.