nunchaku-inria / nunchaku

Model finder for higher-order logic
https://nunchaku-inria.github.io/nunchaku/
BSD 2-Clause "Simplified" License
42 stars 3 forks source link

Release page returns 403 error, and compiling nunchaku fails with numerous errors #37

Open nano-o opened 1 year ago

nano-o commented 1 year ago

Hello, couldn't install nunchaku on my system because the release page https://gforge.inria.fr/projects/nunchaku returns a 403 error and installing with opam (or compiling manually) fails with:

#=== ERROR while compiling nunchaku.0.6 =======================================#
# context     2.1.2 | linux/x86_64 | ocaml.4.13.1 | pinned(git+https://github.com/nunchaku-inria/nunchaku.git#master#91e62687)
# path        ~/.opam/default/.opam-switch/build/nunchaku.0.6
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p nunchaku -j 19
# exit-code   1
# env-file    ~/.opam/log/nunchaku-147734-090624.env
# output-file ~/.opam/log/nunchaku-147734-090624.out
### output ###
# [...]
# Alert deprecated: module CCOpt
# use CCOption instead
# File "src/transformations/TypeInference.ml", line 965, characters 8-17:
# 965 |         CCOpt.map
#               ^^^^^^^^^
# Alert deprecated: module CCOpt
# use CCOption instead
# File "src/transformations/TypeInference.ml", line 1129, characters 22-32:
# 1129 |                       CCOpt.iter (check_prenex_types_ ~loc) g;
#                              ^^^^^^^^^^
# Alert deprecated: module CCOpt
# use CCOption instead

Fixing that with a simple search and replace uncovers more deprecation errors.

c-cube commented 1 year ago

Hi! Thank you for the issue. Have you tried building the master branch?

nano-o commented 1 year ago

Hi, thanks for your response. That's on the master branch. Looking at output again, there are also errors like this:

File "src/parsers/dune", line 11, characters 0-102:
11 | (menhir
12 |   ;(flags (--infer))
13 |   (modules Tip_parser TPTP_parser TPTP_model_parser Parser Parse_kodkod))
Error: the code back-end requires the type of every nonterminal symbol to be
known. Please specify the type of every symbol via %type declarations, or
enable type inference (look up --infer in the manual).
Type inference is automatically enabled when Menhir is used via Dune,
provided the dune-project file says (using menhir 2.0) or later.
The types of the following nonterminal symbols are unknown:
and_form
atomic_form
form
list(statement)
name
or_form
separated_nonempty_list(COMMA,term)
separated_nonempty_list(COMMA,var)
statement
term
unary_form
var

After digging a little more I realized I did not have tip-parser installed. After installing tip-parser with opam (which downgraded menhir-related packages), and also installing qcheck (which is not mentioned in the dependencies in the README), it finally compiled.

Sorry for the confusion.

c-cube commented 1 year ago

No worries. It's a bit complicated to keep up with menhir sometimes.