Skip to content

The bitvector library should ideally be accessible from the main coq-released repository

Ideally we would like the bitvector library in stdpp-unstable to be accessible from Coq Released repository. We need this because we'd like to put the Stdpp version of coq-sail on it. Options includes:

  • Putting stdpp-unstable on Coq Released
  • Merging it in core Stdpp (Tracking issue #145 and #146)
  • Creating a standalone stdpp-bitvector or stdpp-bitvectors or stdpp-bv and ship it to Coq Released separately.

What do you think of those options?