rocq-bignums no longer builds on Rocq dev

[tchajed]

I'm getting an error in CI, which I can reproduce locally:

  # File "plugin/bignums_syntax.ml", line 95, characters 28-61:
  # 95 |       DAst.make ?loc (GInt (PrimNotations.int63_of_pos_bigint n))
  #                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  # Error: Unbound module PrimNotations

This seems to have broken a week ago, July 29; my CI started failing for iris-named-props: https://github.com/tchajed/iris-named-props/actions/runs/16594467766/job/46937683335.

[proux01]

Rocq CI is green so there is likely something out of sync in your setup (be it Rocq itself, Stdlib or bignums that is not master).

[SkySkimmer]

PrimNotations is new so you have bignums more recent than rocq
rocq-prover/rocq#20926 / #103

[tchajed]

My version of rocq dev is out-of-date due to upstream issues in docker-rocq, which hasn't been updated in 11 days (https://hub.docker.com/r/rocq/rocq-prover/tags?page=1&name=dev). I'll just wait for that to get fixed.

[ybertot]

There is progress on docker images for rocq-prover (rocq-community/docker-rocq#17).