ssrmatching.v & Coq 8.6 : what about adding a "transitional" ssrmatching.v file? about math-comp HOT 5 CLOSED

Hi math-comp devs,
Would you have an objection to the solution I had proposed in this issue?
IMHO it would yield a simple and non-intrusive way to provide backward compatibility (and this strategy could be applied likewise if another math-comp theory is integrated in Coq in 8.8 or 8.9 etc.)
If it helps discussing the relevancy of my suggestion, I can prepare a PR.
Kind regards, Erik

from math-comp.

Hi @CohenCyril, OK thanks for your reply, I'm going to push a PR.

from math-comp.

On second thought, adding a quasi-empty file ssrmatching.v in MathComp for compatibility is maybe not very elegant... so feel free to close this issue if you consider that this solution is not worth it.

from math-comp.

As the latest release 1.6.4 of MathComp is compatible with Coq >= 8.5, this question may be still topical.

Actually I need to refine a bit what I had suggested in the initial description:

• the plan would be to add some file ssrmatching.v containing Require Export ssrmatching. in folder mathcomp/ssreflect (not in folder mathcomp/ssreflect/plugin/v8.6)
• for Coq 8.4 and 8.5, this quasi-empty file ssrmatching.v would be symlinked/replaced with the file ssrmatching.v taken from the appropriate plugin subfolder thanks to Makefile.coq-makefile.

Admittedly it would be a not-very-elegant solution for compatibility, but for example it would facilitate the compilation of CoqEAL (which relies on MathComp and ssrmatching) with Coq 8.5 + Coq 8.6 etc., keeping the same Coq theories for any version of Coq and needing no extra configure code in CoqEAL.

@gares @maximedenes @CohenCyril, do you have an opinion on this suggestion?

from math-comp.

I'm not sure I understand, but please prepare a PR.

from math-comp.