remove NArith.Ndigits, NArith.Ndist, and Strings.ByteVector

[andres-erbsen]

• Added / updated test-suite.
• Added changelog.
• Added / updated documentation.

Backwards-compatible overlays:

• directly Require Vector in Lib.Core mit-plv/rupicola#115
• do not depend on Ndigits rocq-community/bignums#90
• remove unneeded Ndigits dependency (adapt to coq/coq#18936) rocq-community/corn#206
• Do not use Ndigits in NUtil (coq/coq #18936) mit-plv/fiat-crypto#1876 -legacy
• stdpp
• iris
• bump stdpp (adapt to coq/coq#18936) mit-pdos/perennial#65

[Alizter]

LGTM. It's been a while since I've reviewed. What was the policy on stdlib deprecations? Is a single version enough? I seem to recall complaints in the past, but that might have been Coq related rather than the stdlib.

[andres-erbsen]

IIUC the closest thing to a policy is https://inria.hal.science/tel-02451322v1/document 3.6.3.1 saying "features must be deprecated in one major version before they can be removed in the next", without any distinction between stdlib or otherwise.

In cep 86 I argue that the duration of deprecation is less important than whether there is an actionable porting plan. For stdlib changes, the worst case of copy-pasting the file removed from Coq does not seem too bad (well, I guess the worst worst case would be Inductive natinf being somehow used in an interface between two non-CI projects for which Coq is the only common dependency, but in this specific case option nat would be a good standin and I don't think this is likely enough to warrant an exceptionally long deprecation regardless).

[proux01]

IIUC the closest thing to a policy is https://inria.hal.science/tel-02451322v1/document 3.6.3.1 saying "features must be deprecated in one major version before they can be removed in the next", without any distinction between stdlib or otherwise.

Note that this is now in the refman: https://coq.inria.fr/doc/V8.19.0/refman/using/libraries/writing.html

@andres-erbsen please list the overlays in the top message

If overlays can be merged before the branch https://github.com/coq/coq/wiki/Release-Schedule-for-Coq-8.20 this seems good for 8.20.

[coqbot-app]

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

✔️ Corresponding jobs for the base commit 7b9f69f 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-iris, ci-perennial

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

[andres-erbsen]

@coqbot run full ci

[Alizter]

@coqbot merge now