deprecate Bvector

[andres-erbsen]

Let's consider deprecating Bvector. It is one of the cases where the additional power of Inductive Vector is not useful, and the file itself acknowledges challenges for reasoning. I am also not aware of any active development using this file. and there seems to be one small intentional maintenance-mode use on CI. Later, I intend for Zmod to be usable for the same stuff as Bvector, and I would be willing to implement a polyfill for the same interface if a user requests it. In addition to reducing needless promotion of Vector, another goal of being proactive with this deprecation is to find out about current uses of Bvector.

• Added changelog.

Overlays for potential removal:

• do not depend on Coq.Bool.Bvector adampetcher/fcf#47 (uses definitions of Bvector, xor, '0)
• Require Vector directly instead of through Bvector equations#589
• fiat-parsers seems to similarly Require Import Bvector without using the definitions
• Despite name matches for definitions in these developments, I have nothing concerning in grep -i error smtcoq.log neural_net_interp.log hott.log flocq.log cross_crypto.log

See also:

• remove NArith.Ndigits, NArith.Ndist, and Strings.ByteVector #18936

[proux01]

Have you run a CI with the removal to see whether it's used in CI?

[andres-erbsen]

I have run make ci-all with the removal and seen some unrelated-looking failures, the list of overlays above is based on investigation of these. I did not kick off a full CI run on INRIA infra because it seems hosed, with light CI for this PR remaining queued for 12h.

[proux01]

I'll merge by the end of next week if there are no more comments.

[andres-erbsen]

@coqbot run full ci

[proux01]

@coqbot run full ci

[proux01]

@coqbot merge now