Stream: Equations devs & users

Topic: Install from source error

Tomás Díaz (Feb 09 2023 at 15:57):

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

Karl Palmskog (Feb 09 2023 at 15:58):

the master branch of Equations is only compatible with Coq's master branch (or coq.dev opam package)

Karl Palmskog (Feb 09 2023 at 15:59):

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.

Tomás Díaz (Feb 09 2023 at 17:51):

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?

Matthieu Sozeau (Feb 09 2023 at 17:53):

Coq’s API changes incompatibly between major versions

Last updated: Jun 11 2023 at 00:30 UTC