math-comp-field-extra

[CohenCyril]

@clarus I just realized that this package was added and committed in 51d4388 with maintainer "Mathematical Components [email protected]". 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]

Indeed, I did not remember it. I found the related issue: #802 I should have mentioned mathcomp developers though.

[palmskog]

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]

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]

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.