Stream: Equations devs & users

Topic: Install from source error


view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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