Remove deprecated files in Arith and Numbers/Natural

[Villetaneuse]

• Removed in Arith:

  • Div2.v
  • Even.v
  • Gt.v
  • Le.v
  • Lt.v
  • Max.v
  • Minus.v
  • Min.v
  • Mult.v
  • Plus.v
  • Arith_prebase.v

• Removed Numbers/Natural/Peano/NPeano.v

• Many "Require" statements involving these files removed in other parts of the library

• Several deprecated lemmas removed in Arith/EqNat

• Register commands moved from Arith_prebase to PeanoNat

• arith hint database moved from Arith_prebase to Arith_base

• Lemmas in Arith_base used only for the hint database have been blacklisted from Search

• Some test files had to change:

  • bugs/bug_13307.v
  • bugs/bug_1779.v
  • bugs/bug_4187.v
  • bugs/bug_4456.v
  • modules/Nat.v
  • success/Funind.v
  • success/RecTutorial.v
  • success/Require.v (Not sure about this one)
  • success/extraction.v
  • success/import_lib.v

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.

Overlays (to be merged before this PR)

• fiat_crypto_legacy Adapt wrt Coq/Coq#18164 mit-plv/fiat-crypto#1738
• Adapt to https://github.com/coq/coq/pull/18164 PrincetonUniversity/VST#747
• Iris https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/535
• Adapt to Coq/Coq#18164 coq-community/corn#202
• Modify examples and tests for Coq/Coq#18164 mattam82/Coq-Equations#570
• Adapt wrt to Coq/Coq#18164 QuickChick/QuickChick#344
• fix arith deprecations coq-community/atbr#40
• Remove deprecated files in Coq.Arith coq-community/autosubst#33
• Remove deprecated files in Coq.Arith mit-plv/bbv#47
• bedrock2 should be ok with Adapt w.r.t Coq#18164 mit-plv/kami#37
• Adapt to Coq/Coq#18164 fblanqui/color#49
• https://gitlab.inria.fr/coquelicot/coquelicot/-/merge_requests/11
• cross_crypto in progress Adapt to Coq/Coq#18164 mit-plv/cross-crypto#34 and Adapt to Coq/Coq#18164 adampetcher/fcf#45 should be ok once the fcf submodule is bumped
• Adapt to Coq/Coq#18164 coq-community/coq-dpdgraph#126
• TODO fiat_parsers
• https://gitlab.inria.fr/flocq/flocq/-/merge_requests/23
• Adapt ro https://github.com/coq/coq/pull/18164 math-comp/hierarchy-builder#398
• Adapt to Coq/Coq#18164 DeepSpec/InteractionTrees#260
• Remove deprecated files in Coq.Arith coq-community/math-classes#121
• https://gitlab.inria.fr/fpottier/menhir/-/merge_requests/36 is merged to master but there is a version problem, see Change Menhir branch target in ci-basic_overlay.sh #18189
• metacoq in progress Adapt wrt Coq/Coq#18164 MetaCoq/metacoq#1011
• Adapt to Coq/Coq#18164 Mtac2/Mtac2#394
• Adapt to https://github.com/coq/coq/pull/18164 coq-community/paramcoq#116
• Adapt wrt Coq/Coq#18164 mit-pdos/perennial#57
• Adapt to Coq/Coq#18164 coq-community/coq-ext-lib#140
• Adapt to Coq/Coq#18164 mit-plv/rewriter#119 and Fix Util/Strings/String.v mit-plv/rewriter#123
• remove all references to deprecated Arith modules from genarg tests ejgallego/coq-serapi#365
• Adapt to Coq/Coq#18164 DeepSpec/sf#11
• Adapt w.r.t Coq/Coq#18164 smtcoq/smtcoq#130
• adapt to https://github.com/coq/coq/pull/18164 uds-psl/coq-library-undecidability#210
• Fix deprecations uwplse/verdi-raft#97

[Villetaneuse]

Since the CI is idle on Sunday, I'm running it (I hope it's ok, sorry if it's not) to evaluate how many overlays will be needed.

[Villetaneuse]

@coqbot run full ci

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[proux01]

Wow, that sounds like a lot of work. Feel free to ping the various maintainers so that they update their code.

[proux01]

I should personally handle paramcoq and I could have a look at Flocq.

[Villetaneuse]

Wow, that sounds like a lot of work. Feel free to ping the various maintainers so that they update their code.

Don't you think I should wait for a review before starting these?

[Villetaneuse]

I think I will have to shellscript my way out of this :D

[palmskog]

Both ci-atbr and ci-verdi-raft should be compatible with this PR now.

[Villetaneuse]

Both ci-atbr and ci-verdi-raft should be compatible with this PR now.

• ci-autosubst merged
• ci-bbv submitted not yet merged
• ci-math_classes merged

[proux01]

Wow, that sounds like a lot of work. Feel free to ping the various maintainers so that they update their code.

Don't you think I should wait for a review before starting these?

Well, as far as I can see you are just removing things that were deprecated in 8.16 (three versions ago) so this should be consensual (I mean, if anyone opposes the deprecation, it should have already been discussed by now).

[Villetaneuse]

Wow, that sounds like a lot of work. Feel free to ping the various maintainers so that they update their code.

Don't you think I should wait for a review before starting these?

Well, as far as I can see you are just removing things that were deprecated in 8.16 (three versions ago) so this should be consensual (I mean, if anyone opposes the deprecation, it should have already been discussed by now).

There could be a discussion about what is happening with Arith_prebase, the Search Blacklists and the modified test files.
But you're right, it does not harm to modify the external libs anyway.

[proux01]

ci-paramcoq should now work and I have a merge request for Flocq that I'll submit when Inria gitlab is back tomorrow.

[Villetaneuse]

ci-paramcoq should now work and I have a merge request for Flocq that I'll submit when Inria gitlab is back tomorrow.

Thank you very much!

[coqbot-app]

🔴 CI failures at commit 9199776 without any failure in the test-suite

✔️ Corresponding jobs for the base commit cb76d6a succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-cross_crypto, ci-fiat_crypto, ci-fiat_crypto_ocaml, ci-fiat_parsers

• You can also pass me a specific list of targets to minimize as arguments.

[coqbot-app]

🔴 CI failures at commit 0521c8f without any failure in the test-suite

✔️ Corresponding jobs for the base commit cb76d6a succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-cross_crypto, ci-fiat_crypto, ci-fiat_crypto_ocaml, ci-fiat_parsers

• You can also pass me a specific list of targets to minimize as arguments.

[proux01]

As agreed during the last meeting, putting the last failing CI entries in allow_failure mode (so that their maintainers can take care of them at their own pace) and merging.

@coqbot merge now

[JasonGross]

As agreed during the last meeting, putting the last failing CI entries in allow_failure mode (so that their maintainers can take care of them at their own pace) and merging.

I don't think this is reasonable, especially for Fiat Crypto.

1. It seems to me that this violates the CI agreement:

Any time that a proposed change is breaking your project, Coq developers and contributors will send you patches to adapt it or will explain how to adapt it and work with you to ensure that you manage to do it.

2. If I recall correctly, the last time a PR was merged that broke Fiat Crypto, in the intervening week that it took too fix Fiat Crypto, another PR broke Fiat Crypto in a different way without realizing it, because the CI wasn't testing Fiat Crypto
3. I'm currently very busy and don't really have time to make intensive changes to these projects. If the changes are not intensive I would have appreciated you submitting PRs. If the changes are intensive I think we should reconsider the backwards compatibility policy with respect to the automation that should be provided for fixing changes.
4. I don't understand what the rush is to merge this PR. As I understand it, there is nothing that depends on this PR, nothing blocked on this PR being merged, and merging this PR, while it does clean up the standard library somewhat, does not significantly improve Coq relative to the cost that it imposes such that it should be rushed into Coq at the cost of breaking a handful of CI developments.
5. This breaks Fiat Crypto's deploy workflow, which was set up on the presumption that Coq wouldn't needlessly break our build.

I'm sorry that I haven't had the time to prepare patches for the projects I (co)maintain to adapt to this PR, but I'd rather see this reverted than leave the CI in a broken state, especially with projects that frequently catch incompatibilities with Coq.

[SkySkimmer]

As agreed during the last meeting, putting the last failing CI entries in allow_failure mode (so that their maintainers can take care of them at their own pace) and merging.

Is that what we said? the notes say " We really aim to have it before the RC release." nothing about allow_failure

[proux01]

Yes, I even remember checking during the wrapup at the end of the discussion that there was no disagreement on that point. The notes indeed lack precision.

[proux01]

It seems to me that this violates the CI agreement:

Any time that a proposed change is breaking your project, Coq developers and contributors will send you patches to adapt it or will explain how to adapt it and work with you to ensure that you manage to do it.

I disagree, but we should probably edit that sentence as it seems to be often understood (not saying this is the case here) as implying that Coq devs are responsible for CI entries updates, which they are not.

It's also true that we had no effective way to reach out to CI entries maintainers, this should be improved by #18321

I don't understand what the rush is to merge this PR.

We want this in the upcoming RC, otherwise this will only land in the next one, six months later. Not merging PRs in reasonnable time can be discouraging for new contributors, particularly when they already put a lot of effort into them. We already exhausted a few contributors this way and have to be more proactive in merging PRs to avoid discouragement.