[WIP]removed deprecation warnings and most duplicate clear warnings

[ybertot]

Current version has two duplicate-clear warnings that require a little more thinking.

[palmskog]

Note that this PR drops compatibility with Coq 8.11 (due to adding the #[export] hint locality, which did not exist in 8.11). If this is what we want, I can modify meta.yml and CI accordingly.

[ybertot]

I don't understand why you mention only incompatibility with Coq 8.11, Nix CI for bundle 8.12+1.13, 8.13+1.13, 8.12+1.14, 8.13+1.14 are also failures.

I only understood that this branch is premature for backward compatibility.

[palmskog]

You're right that 8.12 and 8.13 are also incompatible (I guess for the same reason with locality). But do you want to modify CI configuration in the same branch right now? Or do it later when it's not WIP anymore?

[ybertot]

I wish to wait until the next math-comp meeting to know what policy should maintained with respect to backward compatibility on the master branch.

For now I am happy to have a branch that contains fixes for many fixable warnings, but I am don't believe all these warning have the same degree of urgency.

• I fixed several deprecation warnings that may not be timed to the same release of Coq or math-comp
• the duplicate-clear warnings don't seem to have a deadline, it is just healthy to get rid of them.

I wanted to make the branch a PR so that potential contributors get a chance to know that this work is indeed in progress. Do you think the README file should be modified to advertise this way of life?

[palmskog]

@ybertot based on my experience in maintaining the RegLang project, I believe a reasonable policy in maintaining a project using MathComp is:

• at all times, support all the Coq versions supported by mathcomp master branch (this implies tolerating some deprecation warnings by Coq)
• if feasible and on a case-by-case basis, support additional Coq versions with MathComp releases; stop supporting these Coq versions to fix deprecation warnings when reasonable

Hence, I think it may be a good idea to separate out deprecation warning fixes that do not drop Coq versions. See for example this RegLang PR, which we will merge when we drop Coq 8.11 support.

[ybertot]

Thanks, I will do as suggested, it may take a few days before I come back to it though.