This repository was archived by the owner on Sep 17, 2026. It is now read-only.
Repository navigation
This repository was archived by the owner on Sep 17, 2026. It is now read-only.
Archiving this repository #56
Description
Should we archive this repository now that stdlib has a bits type? I don't think stdlib implements every single thing that bbv does, but it's been enough for guru and bedrock2 and fiat-crypto. Thus, I think that a future development needing bitvector support would be better of exenting bits than using bbv word. And maybe we can stop maintaining this repository.
Nothing in Rocq CI depends on the target for this repo: gitlab.inria.fr/coq/coq/-/pipelines/1286380
Activity
samuelgruetter commentedon Nov 12, 2025
Makes sense to me!
JasonGross commentedon Mar 2, 2026
Note that coq-sail still depends on this
https://github.com/rems-project/coq-sail/blob/927111b2f61fe6208a7c24539167a7bec5d9d21d/coq-sail.opam#L42
andres-erbsen commentedon Sep 14, 2026
I intend to archive this repository once mit-plv/kami#51 lands.