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

Build fails: Error (warning 70 [missing-mli]): Cannot find interface file. #154

Open yurivict opened 4 months ago

yurivict commented 4 months ago

Build fails on some systems:

ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src -I test/ext -o src/extensions.cmo src/extensions.ml
+ ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src -I test/ext -o src/extensions.cmo src/extensions.ml
File "src/extensions.ml", line 1:
Error (warning 70 [missing-mli]): Cannot find interface file.
Command exited with code 2.
gmake: *** [Makefile:7: all] Error 10
===> Compilation failed unexpectedly.

log

Version: 2.0.7 ocaml-4.14.1 FreeBSD 14.0

chaudhuri commented 4 months ago

Is there a specific reason you are trying to build 2.0.7? 2.0.8 has been out for several months now.

yurivict commented 4 months ago

2.0.8 depends on specific versions of ocaml-dune which isn't available in FreeBSD ports due to conflicts with other ocaml packages.

ocaml-dune-3.7.1 that is available isn't compatible with 2.0.8

chaudhuri commented 4 months ago

Let me check if 2.0.8 compiles with Dune 3.7.1 specifically. A priori it should since it only has (lang dune 3.7).

chaudhuri commented 4 months ago

Looks like the master branch builds with Dune 3.7.1 and works fine at least on Linux. I can release this as Abella 2.0.8.1 if you want. The 2.0.9 release is still a while away.

Sorry, spoke too soon. It seems that the dependency on xdg forces Dune to be upgraded. I guess I can make a patch on top of 2.0.8 before we added the xdg dependency which should hopefully work with Dune 3.7.1.

chaudhuri commented 4 months ago

Please see if the 2.0.8.1 release builds for you.

yurivict commented 3 months ago

2.0.8.1 fails:

dune build src/abella.exe src/abella_doc.exe src/abella_dep.exe
File "src/dune", line 29, characters 34-38:
29 |  (libraries unix re yojson base64 curl)
                                       ^^^^
Error: Library "curl" not found.
-> required by library "abella_lib" in _build/default/src
-> required by executable abella in src/dune:2
-> required by _build/default/src/abella.exe
gmake: *** [Makefile:7: all] Error 1

curl-8.7.1 is installed.

chaudhuri commented 3 months ago

Is the OCaml library ocurl installed? The dependencies are listed in abella.opam -- please make sure all the libraries with their minimum versions are available.