Rm warnings 8.11

[ybertot]

This takes a subset of the changes in #41 and preserves compatibility with coq-8.11 and math-comp 1.11

[ybertot]

@palmskog can you help me? I don't understand why no CI check have been performed for this PR

[palmskog]

@ybertot there was a GitHub outage this Friday that affected CI. The CI will run again if you do a new push (or I can do it if you want).

[ybertot]

Only a push can trigger it?

[palmskog]

To my knowledge, there is no other way. But recall that you can do the following locally to do a "no-operation" push in the branch:

git commit --amend
git push -f

The first command changes the SHA of the last commit without changing its content, and then you push the new state to the upstream branch.

[ybertot]

thks, I just discovered I had modification I had forgotten to push anyway.

[palmskog]

@ybertot this PR looks good now in CI. However, I think we should also stop to ignore the warnings that you fixed here, for example, the following should be removed in _CoqProject and dune files:

-arg -w -arg -implicit-core-hint-db
-arg -w -arg -duplicate-clear

[ybertot]

I don't understand. these lines do not appear in _CoqProject, and there is no dune file.

[ybertot]

@palmskog

[palmskog]

Ah, my mistake, I saw some changes I had done locally. But then we may actually want to add the following into _CoqProject:

-arg -w -arg -ambiguous-paths
-arg -w -arg -deprecated-hint-without-locality
-arg -w -arg -deprecated-instance-without-locality
-arg -w -arg -deprecated-syntactic-definition

... to make the project warning-free during local compilation, and then remove those as more warnings are fixed.

[ybertot]

I had the same interrogations myself. What should be the policy: strive for a warning free compilation at the risk of forgetting the work that needs to be done as deprecation looms, or leave the deprecation warnings (and only these) as a reminder?

I would prefer to silence only the ambiguous-path warning. Would you agree?

[palmskog]

My personal preference is for a warning-free build, with carefully curated GitHub issues and/or draft pull requests to document why some warnings are not addressed (likely due to Coq version compatibility). The main reason is that contributors to a project will not be distracted by irrelevant warnings locally or in the CI.

Still, silencing just the ambiguous-path warning is good as well.

[ybertot]

This made me discover a couple of bugs in the current setup:

1. Makefile.coq.local should never have been checked in, this file is the one that should be used by developers to have their personal choice of warnings removed. The warnings in Makefile.coq.local should be included in the _CoqProject file.
2. Makefile.coq.local refers to a variable OTHERFAGS when it should have been OTHERFLAGS. Because of this, any line of the form "-arg -w -arg -ambiguous-paths" for example, is actually ignored at compilation time.

[ybertot]

I don't know why Makefile.coq.local is not on the master branch, but it is on both my warning removal branches.

[ybertot]

Ok, I found out that @palmskog cleaned up the setup in PR #38, where the flawed Makefile.coq.local was actually removed from the main branch, but this branch has not been rebased yet, so it is still present.

[palmskog]

This now looks ready to merge to me, it's a strict improvement given our current bounds on Coq and MathComp.