I'm trying to build Equations from source but I'm getting the following error:
File "src/equations_common.ml", line 45, characters 2-19:
45 | Goptions.optstage = Interp;
^^^^^^^^^^^^^^^^^
Error: Unbound record field Goptions.optstage
make[2]: *** [src/equations_common.cmx] Error 2
make[1]: *** [all] Error 2
make: *** [all] Error 2
I'm building branch master
on OS X 12.5 with the following settings:
The Coq Proof Assistant, version 8.16.1
compiled with OCaml 4.14.0
Am I missing something? I just did ./configure.sh
and make
the master
branch of Equations is only compatible with Coq's master
branch (or coq.dev
opam package)
we recommend using the latest release for 8.16, or if this is somehow not an option, the 8.16
branch in the Equations repo will compile with 8.16.1.
ok, perfect, thanks :ok: .
Just wondering but the error comes from the .ml file, how does the Coq version have anything to do with that?
Coq’s API changes incompatibly between major versions
Last updated: Jun 11 2023 at 00:30 UTC