search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

[regression in 2.0.8] Error: Version 3.11 of the dune language is not supported. #148

Closed yurivict closed 9 months ago

yurivict commented 9 months ago

The build of the 2.0.8 version fails:

dune build src/abella.exe src/abella_doc.exe src/abella_dep.exe
File "dune-project", line 1, characters 11-15:
1 | (lang dune 3.11)
               ^^^^
Error: Version 3.11 of the dune language is not supported.
Supported versions of this extension in version 3.11 of the dune language:
- 1.0 to 1.12
- 2.0 to 2.9
- 3.0 to 3.7

ocaml-dune-3.7.1 ocaml-ocamlbuild-0.14.2_2 FreeBSD 13.2

chaudhuri commented 9 months ago

Abella has only been tested to build with Dune 3.11+. If you use opam it should automatically upgrade Dune if needed. I'll check in the morning if earlier Dune releases work as well.

yurivict commented 9 months ago

I am trying to upgrade the FreeBSD port, and it has to use packages for ocaml* dependencies.

chaudhuri commented 9 months ago

Lowered the Dune lang to 3.7 in 0c5a1faf45bb627a1a5a86ae588a13ec2791ed4e. Please see if it compiles for you.

Unfortunately it's too late for 2.0.8, but we can release a 2.0.8.1 with this change if you want.

chaudhuri commented 9 months ago

Closing this because this is not a regression. Please fix the dependencies you've listed in your Makefile. Abella's dependencies can be found in the abella.opam file.

chaudhuri commented 4 months ago

Continued in #154