search

coq / opam

Archive for all Coq related OPAM packages organized in various repositories
https://coq.inria.fr/opam/www/
GNU Lesser General Public License v2.1
121 stars 162 forks source link

math-comp-field-extra #1300

Open CohenCyril opened 4 years ago

CohenCyril commented 4 years ago

@clarus I just realized that this package was added and committed in https://github.com/coq/opam-coq-archive/commit/51d43887e025dd7e4da545e4872e135d5b9a769b with maintainer "Mathematical Components mathcomp-dev@sympa.inria.fr". To my knowledge this has not been discussed there, and this package does not correspond to any of our packages, so I am very surprised. Can you tell me the story of this package?

clarus commented 4 years ago

Indeed, I did not remember it. I found the related issue: https://github.com/coq/opam-coq-archive/issues/802 I should have mentioned mathcomp developers though.

palmskog commented 4 years ago

The bottom line is that this package was added by @clarus and myself to preserve an old version of odd-order. It was a mistake to set mathcomp-dev as a maintainer (this was due to us just copying another opam file).

CohenCyril commented 4 years ago

mmh, I see, I would have preferred to copy the missing files from field/ to odd-order/ (and amending odd-order/Makefile accordingly) in the build phase rather than creating an ad-hoc package. Do you think we can alter this safely, or that we should absolutely not touch it, or that we should not care since this is old stuff? (It does pollute the opam-coq-archive repo and opam list forever though)

palmskog commented 4 years ago

Creating a new package was viewed as the most straightforward solution at the time (given that there are already quite a few historical packages).

@CohenCyril if you want to alter the package definition of odd-order.1.6.1, to make the field-extra package obsolete, this is fine by me. But I still think we should keep odd-order.1.6.1 functional in some way.