Dear all,
The Rocq 9.3+rc1 tag has been pushed, opam packages are available in
the core-dev repo and nix packages are merged in the unstable suite.
A compatible Stdlib release and Docker images are on their way.
It is now time to test the release candidate and plan a release of your
packages if need be. The release of 9.3.0 is expected to happen in
about one month.
Many thanks to everybody involved in this release cycle.
Thank your for letting me know. I got an error during the build of the stable version of mathcomp-boot. Maybe dune is incompatible with Rocq 9.3+rc1?
$ opam install rocq-mathcomp-boot -j3
[ERROR] The compilation of rocq-elpi.3.5.0 failed at "etc/with-rocq-wrap.sh dune build -p rocq-elpi -j 3 @install".
#=== ERROR while compiling rocq-elpi.3.5.0 ====================================#
# context 2.5.2 | macos/arm64 | ocaml-base-compiler.4.14.2 | https://rocq-prover.org/opam/released#2026-07-24 13:41
# path ~/.opam/rocq-9.3-rc1/.opam-switch/build/rocq-elpi.3.5.0
# command ~/.opam/opam-init/hooks/sandbox.sh build etc/with-rocq-wrap.sh dune build -p rocq-elpi -j 3 @install
# exit-code 1
# env-file ~/.opam/log/rocq-elpi-44121-150615.env
# output-file ~/.opam/log/rocq-elpi-44121-150615.out
### output ###
# ++ command -v rocq
# + rocq=/Users/yosukeito/.opam/rocq-9.3-rc1/bin/rocq
# +++ dirname etc/with-rocq-wrap.sh
# ++ dune exec --root etc/.. -- etc/tools/hash.exe
# File "dune-project", line 2, characters 0-15:
# 2 | (using coq 0.8)
# ^^^^^^^^^^^^^^^
# Error: Extension coq was deleted in the 3.24 version of the dune language
# Hint: The Coq Build Language has been replaced by the Rocq Build Language.
# Use (using rocq <version>) instead.
# + rocqhash=
I apologize if it is not the right place to report.