Rocq 9.3.0

Announcements
1

We are happy to announce that Rocq 9.3.0 has been released and packages for opam and nix are available.

See the changelog Recent changes — The Rocq Prover 9.3.0 documentation for more information.

— Enrico for the Rocq Development Team.

2

Thank you very much. However, I got an error as follows (macOS 26.6.2):

% opam install rocq-prover rocq-core=9.3.0
The following actions will be performed:
=== install 9 packages
  ∗ conf-gmp        5      [required by zarith]
  ∗ conf-pkg-config 5      [required by zarith]
  ∗ dune            3.24.2 [required by rocq-core]
  ∗ ocamlfind       1.9.8  [required by rocq-runtime]
  ∗ rocq-core       9.3.0
  ∗ rocq-prover     meta.1
  ∗ rocq-runtime    9.3.0  [required by rocq-core]
  ∗ rocq-stdlib     dev    [required by rocq-prover]
  ∗ zarith          1.14   [required by rocq-runtime]

Proceed with ∗ 9 installations? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫 
⬇ retrieved conf-gmp.5  (cached)
⬇ retrieved conf-pkg-config.5  (cached)
⬇ retrieved ocamlfind.1.9.8  (cached)
∗ installed conf-pkg-config.5
∗ installed conf-gmp.5
⬇ retrieved rocq-stdlib.dev  (git+https://github.com/coq/stdlib.git#master)
⬇ retrieved zarith.1.14  (cached)
⬇ retrieved rocq-core.9.3.0, rocq-runtime.9.3.0  (https://opam.ocaml.org/cache)
⬇ retrieved dune.3.24.2  (https://opam.ocaml.org/cache)
∗ installed ocamlfind.1.9.8
∗ installed zarith.1.14
∗ installed dune.3.24.2
[ERROR] The compilation of rocq-runtime.9.3.0 failed at "./configure -release -relocatable -native-compiler no".

#=== ERROR while compiling rocq-runtime.9.3.0 =================================#
# context     2.5.2 | macos/arm64 | ocaml-base-compiler.4.14.2 | https://opam.ocaml.org#6f927382c92d816a9b54225f9aeae9c52d0e5e10
# path        ~/.opam/rocq-9.3/.opam-switch/build/rocq-runtime.9.3.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build ./configure -release -relocatable -native-compiler no
# exit-code   139
# env-file    ~/.opam/log/rocq-runtime-4196-355f82.env
# output-file ~/.opam/log/rocq-runtime-4196-355f82.out
### output ###
# ./configure: line 21:  9789 Segmentation fault: 11  dune exec $dune_release --root . -- $configure "$@"



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫 
┌─ The following actions failed
│ λ build rocq-runtime 9.3.0
└─ 
┌─ The following changes have been performed (the rest was aborted)
│ ∗ install conf-gmp        5
│ ∗ install conf-pkg-config 5
│ ∗ install dune            3.24.2
│ ∗ install ocamlfind       1.9.8
│ ∗ install zarith          1.14
└─

Is the dune issue #16417 related with the error? If so, I would like to know a recommended workaround. I apologize if the above error is due to my specific problem.

3

Hello, this forum is for announcements.

I recommend you post your issue in the zuilp stream Public view of The Rocq Prover | Zulip team chat or open a github issue directly.

4

I am sorry for the wrong post. Thank you for your suggestion.