fourcolor icon indicating copy to clipboard operation
fourcolor copied to clipboard

Published 20 hours ago • verified publisher icon coq-community

[WIP]removed deprecation warnings and most duplicate clear warnings

Open ybertot opened this issue 2 years ago • 6 comments

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

ybertot avatar Mar 13 '22 20:03 ybertot

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.

palmskog avatar Mar 14 '22 09:03 palmskog

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.

ybertot avatar Mar 14 '22 15:03 ybertot

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?

palmskog avatar Mar 14 '22 16:03 palmskog

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?

ybertot avatar Mar 15 '22 07:03 ybertot

@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.

palmskog avatar Mar 23 '22 10:03 palmskog

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

ybertot avatar Mar 23 '22 10:03 ybertot