Build error with coq-prosa.dev
Hi,
I am using Coq 8.17. I get the following error when trying to install coq-prosa from Opam
➜ crazyflie git:(master) ✗ opam install coq-prosa
The following actions will be performed:
∗ install coq-prosa dev
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
⬇ retrieved coq-prosa.dev (no changes)
[ERROR] The compilation of coq-prosa.dev failed at "make -j7".
#=== ERROR while compiling coq-prosa.dev ======================================#
# context 2.1.2 | macos/x86_64 | ocaml-system.4.12.0 | https://coq.inria.fr/opam/extra-dev#2023-05-14 09:10
# path ~/.opam/default/.opam-switch/build/coq-prosa.dev
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j7
# exit-code 2
# env-file ~/.opam/log/coq-prosa-24942-cd9c6f.env
# output-file ~/.opam/log/coq-prosa-24942-cd9c6f.out
### output ###
# [...]
# COQC util/rel.v
# COQC util/seqset.v
# COQC util/epsilon.v
# COQC util/setoid.v
# COQC util/int.v
# File "./util/seqset.v", line 19, characters 36-44:
# Error: Syntax error: [reduce] expected after ':=' (in [def_body]).
#
# make[2]: *** [util/seqset.vo] Error 1
# make[2]: *** Waiting for unfinished jobs....
# make[1]: *** [all] Error 2
# make: *** [prosa] Error 2
Is this configuration tested in your CI/CD env? All my other Coq packages have been installed through opam, that I would expect my env. to be up to date.
Thanks
Edited by Jerome Hugues