opam installation failed for OCaml 4.03.0

[samuelgruetter]

On an opam switch with OCaml 4.03.0, I ran

opam pin add -k git nunchaku https://github.com/nunchaku-inria/nunchaku.git#master

but I got the following error:

nunchaku is now git-pinned to https://github.com/nunchaku-inria/nunchaku.git#master

[nunchaku] https://github.com/nunchaku-inria/nunchaku.git#master updated

nunchaku needs to be installed.
The following actions will be performed:
  - install jbuilder   1.0+beta20                       [required by nunchaku]
  - install ocamlbuild 0.12.0                           [required by menhir, sequence]
  - install result     1.3                              [required by containers]
  - install uchar      0.0.2                            [required by containers]
  - install sequence   0.5.4                            [required by nunchaku]
  - install menhir     20180905                         [required by nunchaku]
  - install containers 2.3                              [required by nunchaku]
  - install nunchaku   0.5.1*    
===== 8 to install =====
Do you want to continue ? [Y/n] y

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[default] https://opam.ocaml.org/1.2.2/archives/containers.2.3+opam.tar.gz downloaded
[default] https://opam.ocaml.org/1.2.2/archives/jbuilder.1.0+beta20+opam.tar.gz downloaded
[ocamlbuild] Archive in cache
[nunchaku] https://github.com/nunchaku-inria/nunchaku.git#master already up-to-date
[default] https://opam.ocaml.org/1.2.2/archives/menhir.20180905+opam.tar.gz downloaded
[default] https://opam.ocaml.org/1.2.2/archives/result.1.3+opam.tar.gz downloaded
[default] https://opam.ocaml.org/1.2.2/archives/sequence.0.5.4+opam.tar.gz downloaded
[default] https://opam.ocaml.org/1.2.2/archives/uchar.0.0.2+opam.tar.gz downloaded

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-> installed ocamlbuild.0.12.0
-> installed uchar.0.0.2
-> installed jbuilder.1.0+beta20
-> installed result.1.3
-> installed sequence.0.5.4
-> installed containers.2.3
-> installed menhir.20180905
[ERROR] The compilation of nunchaku failed at "jbuilder build -p nunchaku -j 4".

#=== ERROR while installing nunchaku.0.5.1 ====================================#
# opam-version 1.2.2
# os           linux
# command      jbuilder build -p nunchaku -j 4
# path         /home/sam/.opam/smtcoq_cvc4/build/nunchaku.0.5.1
# compiler     4.03.0
# exit-code    1
# env-file     /home/sam/.opam/smtcoq_cvc4/build/nunchaku.0.5.1/nunchaku-25480-722625.env
# stdout-file  /home/sam/.opam/smtcoq_cvc4/build/nunchaku.0.5.1/nunchaku-25480-722625.out
# stderr-file  /home/sam/.opam/smtcoq_cvc4/build/nunchaku.0.5.1/nunchaku-25480-722625.err
### stderr ###
# Warning: the token SECTION is unused.
# [...]
# (cd _build/default && /home/sam/.opam/smtcoq_cvc4/bin/ocamlc.opt -w -40 -w +a-4-42-44-48-50-58-32-60-29@8 -color always -g -bin-annot -I src/core/.nunchaku_core.objs -I /home/sam/.opam/smtcoq_cvc4/lib/bytes -I /home/sam/.opam/smtcoq_cvc4/lib/containers -I /home/sam/.opam/smtcoq_cvc4/lib/containers/data -I /home/sam/.opam/smtcoq_cvc4/lib/containers/monomorphic -I /home/sam/.opam/smtcoq_cvc4/lib/num -I /home/sam/.opam/smtcoq_cvc4/lib/ocaml/threads -I /home/sam/.opam/smtcoq_cvc4/lib/result -I /home/sam/.opam/smtcoq_cvc4/lib/sequence -I /home/sam/.opam/smtcoq_cvc4/lib/uchar -no-alias-deps -open Nunchaku_core -o src/core/.nunchaku_core.objs/nunchaku_core__FO.cmo -c -impl src/core/FO.ml)
# File "src/core/FO.ml", line 318, characters 7-26:
# Error: Unbound value Sequence.flat_map_l
# Hint: Did you mean flat_map?
#     ocamlopt src/core/.nunchaku_core.objs/nunchaku_core__FO.{cmx,o} (exit 2)
# (cd _build/default && /home/sam/.opam/smtcoq_cvc4/bin/ocamlopt.opt -w -40 -w +a-4-42-44-48-50-58-32-60-29@8 -color always -g -bin-annot -O2 -I src/core/.nunchaku_core.objs -I /home/sam/.opam/smtcoq_cvc4/lib/bytes -I /home/sam/.opam/smtcoq_cvc4/lib/containers -I /home/sam/.opam/smtcoq_cvc4/lib/containers/data -I /home/sam/.opam/smtcoq_cvc4/lib/containers/monomorphic -I /home/sam/.opam/smtcoq_cvc4/lib/num -I /home/sam/.opam/smtcoq_cvc4/lib/ocaml/threads -I /home/sam/.opam/smtcoq_cvc4/lib/result -I /home/sam/.opam/smtcoq_cvc4/lib/sequence -I /home/sam/.opam/smtcoq_cvc4/lib/uchar -no-alias-deps -open Nunchaku_core -o src/core/.nunchaku_core.objs/nunchaku_core__FO.cmx -c -impl src/core/FO.ml)
# File "src/core/FO.ml", line 318, characters 7-26:
# Error: Unbound value Sequence.flat_map_l
# Hint: Did you mean flat_map?

=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
  - install nunchaku 0.5.1
The following changes have been performed
  - install containers 2.3       
  - install jbuilder   1.0+beta20
  - install menhir     20180905  
  - install ocamlbuild 0.12.0    
  - install result     1.3       
  - install sequence   0.5.4     
  - install uchar      0.0.2     

=-=- containers.2.3 installed successfully =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
=> Containers 2.3 is a small release with a few more functions in existing modules,
   some bugfixes, and many performance improvements.

   Changelog: https://github.com/c-cube/ocaml-containers/blob/2.3/CHANGELOG.adoc
[NOTE] Pinning command successful, but your installed packages may be out of sync.

The former state can be restored with:
    opam switch import "~/.opam/smtcoq_cvc4/backup/state-20180912230059.export"

This is surprising because according to this travis build, OCaml 4.03.0 should be supported.

Any advice on how to get this to build?

[c-cube]

For some reason your opam has installed a really old version of sequence (from 2014). I just added a lower bound to the opam file.

[c-cube]

Unrelated, but you may want to migrate to opam 2. opam 1's repository is now frozen and new packages won't show on it.

I plan to update nunchaku's opam file to the 2.0 format soon.

[samuelgruetter]

Thanks for the fix, installation succeeded!

Now I tried to run it on the sample file mentioned in the README (which turns out to be not exactly at docs/examples/first_order.nun, but I took nunchaku-problems/tests/first_order.nun).

So I ran

nunchaku tests/first_order.nun

but got

Error: in the interface to CVC4: non first-order list

Output of cvc4 --version:

This is CVC4 version 1.7-prerelease [git master 9168f325]
compiled with GCC version 8.1.1 20180712 (Red Hat 8.1.1-5)
on Oct 10 2018 01:26:41

[c-cube]

I think this deserves its own issue. I don't have cvc4 1.7 though :s

[samuelgruetter]

Thanks for the hint, so I tried with CVC4 version 1.5 (the one shipped with Isabelle2017), and it worked! The separate issue is here: https://github.com/nunchaku-inria/nunchaku/issues/27