Remove MC2.4 deprecations and cleanup mathcomp_extra.v

[pi8027]

Motivation for this change

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[pi8027]

I added these attributes (see below) since I prepared this PR by adding the following lines to _CoqProject:

-arg -w -arg +deprecated-reference
-arg -w -arg +deprecated-syntactic-definition
-arg -w -arg +deprecated-notation

Since they are the internal use of deprecated definitions/lemmas, I think that suppressing the deprecation warning here is the right thing to do, but feel free to revert this part of the changes.

Since these deprecations date back to 3 years ago, removing all of them is also an option.

[pi8027]

I didn't manage to get rid of full_fsbigID here.

[pi8027]

(IMO, we should have added -arg -w -arg +deprecated-since-mathcomp-2.4.0 to _CoqProject when we require MC 2.4.)

[affeldt-aist]

Thanks for having taken care of that!
As for the warnings in Rstruct.v, I don't have a strong opinion, apart from the fact that this file should be cleaned. :-(
The only development that I can think of that might depend on that is Damien and Cyril's work on LaSalle and the pendulum @CohenCyril . We have recently ported the latter to the last version of MathComp-Analysis, so it will be easy to confirm soon whether it is really needed or not and do cleaning accordingly (I'll try to do that asap).

[pi8027]

Then, shall we merge this as is, and decide what to do with Rstruct.v later?

[CohenCyril]

Then, shall we merge this as is, and decide what to do with Rstruct.v later?

Suppressed deprecation warnings are very likely to cause unanticipated bugs in the future. I'm still ok with merging asap as long as we open an issue.

From the above discussion, I did not manage to understand the exact cause of the failure to replace deprecated defs/notations/lemmas by non deprecated ones. Can someone explain?

[pi8027]

From the above discussion, I did not manage to understand the exact cause of the failure to replace deprecated defs/notations/lemmas by non deprecated ones. Can someone explain?

The ones in Rstruct.v are a deprecated definition bigmaxr and some deprecated lemmas about it. These lemmas depend on bigmaxr and some other deprecated lemmas. I consider them as an "internal use" of deprecated definitions and lemmas, and thus, I think that these deprecation warnings are safe to suppress.

To be clear, it's also ok to remove these #[warning="-deprecated"].

[pi8027]

IMO, the compilation of MCA produces too many warnings, and it makes it hard to understand which ones have to be fixed. So, if I'm the one maintaining it, I would suppress the ones that are totally safe to ignore, e.g., the ones about unstable.v.

[affeldt-aist]

I am in favor of merging almost as it is (I'll maybe remove the #[warning="-deprecated"] in Rstruct.v: it looks a bit too verbose for something that could very well disappear as soon as someone really looks into it). As for the quantity of warnings, I am ok with a status-quo: we are not overwhelmed and, for having recently ported Damien's development, I found the warnings helpful (also, we rely on unstable.v in infotheo).

[pi8027]

You should indeed be warned when you use unstable.v outside MCA, but we can suppress this warning in MCA by adding the #[warning=...] attribute to Require Import.

[affeldt-aist]

The only development that I can think of that might depend on that is Damien and Cyril's work on LaSalle and the pendulum @CohenCyril . We have recently ported the latter to the last version of MathComp-Analysis, so it will be easy to confirm soon whether it is really needed or not and do cleaning accordingly (I'll try to do that asap).

No, it is not using it.

trajectories is also using "bigmax" but this is a redefinition that is actually superseded by order.v
(NB: you might need MC 2.5.0 for some lemmas @ybertot )

https://github.com/math-comp/trajectories/blob/022aeb4097e91faf05cd1ec7b7d91e72e3c83315/theories/pol.v#L127

infotheo is also using a redefinition of bigmax but seems to be using MC's lemma already
(or it's maybe the other war around)

I can't think of any development that uses the bigmaxr definition of Rstruct (@t6s ?), shall we just get rid of it?

[t6s]

I can't think of any development that uses the bigmaxr definition of Rstruct (@t6s ?), shall we just get rid of it?

Me neither. Let's remove it.