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: *** [src/equations_common.cmx] Error 2 make: *** [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
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: Sep 28 2023 at 11:01 UTC