2019-10-31 15:22:24 (GMT)
Hi. I am attempting to compile Zipperposition (for the first time). I have attempted to follow the instructions on the git page, but am receiving the following error:
mbaxwab3@cslap02:~/zipperposition$ opam install zipperposition
The following dependencies couldn't be met:
- zipperposition → containers < 2.0 → ocaml < 4.08.0
base of this switch (use `--unlock-base' to force)
- zipperposition → sequence >= 0.4 → ocaml < 4.08.0
base of this switch (use `--unlock-base' to force)
No solution found, exiting
The version of opam being used is 2.0.4. I have tried re-intialising opam with the command: opam init --compiler=4.07.0 with no success. Pretty sure, I must be doing something basic wrong. Any ideas?
2019-10-31 16:9:6 (GMT)
Hi @Ahmed B ! Are you compiling from the sources? Or directly with opam install zipperposition?
2019-10-31 16:22:19 (GMT)
Also, it's most likely not you; opam is sometimes hard to use properly, and OCaml 4.08 support is still a bit, hum, fresh.
2019-10-31 16:25:29 (GMT)
@Simon Cruanes Not sure what you mean by "compiling from the sources". I've cloned the Zipperposition repo onto my machine, installed opam and then run opam install zipperposition in the repo whilst on the lzip branch.
2019-10-31 16:26:22 (GMT)
Ah yes, opam install doesn't care where you are. You could try opam pin .#HEAD in the repo and it should install the proper dependencies too.
2019-10-31 17:37:44 (GMT)
@Petar Vukmirovic what's a stable branch for Ahmed to try and compile? I know master builds but it doesn't contain most of the HO stuff.
2019-10-31 18:17:28 (GMT)
I would suggest the branch lzip-bool, which is basically what entered CASC this year, or the branch unif_framework, which contains Petar's most recent changes to the unification module.
2019-10-31 18:20:54 (GMT)
Good point. I just updated it so it compiles on my machine.
2019-10-31 18:23:21 (GMT)
We really need to pay attention to CI for the release :sweat_smile:
2019-10-31 20:34:10 (GMT)
Still no luck. When I try to compile the lzip-bool branch, this:
#=== ERROR while compiling libzipperposition.1.5 ==============================#
# context 2.0.4 | linux/x86_64 | ocaml-base-compiler.4.09.0 | pinned(git+file:///home/mbaxwab3/zipperposition#HEAD#88f993e4)
# path ~/.opam/default/.opam-switch/build/libzipperposition.1.5
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p libzipperposition
# exit-code 1
# env-file ~/.opam/log/libzipperposition-15185-d8a4ae.env
# output-file ~/.opam/log/libzipperposition-15185-d8a4ae.out
### output ###
# Prop (_, _)
# [...]
# (cd _build/default && /home/mbaxwab3/.opam/default/bin/ocamlc.opt -w -40 -warn-error -3 -color always -safe-string -w -32-50 -g -bin-annot -I src/prover_calculi/.libzipperposition_calculi.objs/byte -I /home/mbaxwab3/.opam/default/lib/bytes -I /home/mbaxwab3/.opam/default/lib/containers -I /home/mbaxwab3/.opam/default/lib/containers/data -I /home/mbaxwab3/.opam/default/lib/containers/monomorph[...]
# File "src/prover_calculi/superposition.ml", line 167, characters 21-47:
# 167 | let cached_t = Subst.FO.canonize_all_vars t in
# ^^^^^^^^^^^^^^^^^^^^^^^^^^
# Error: Unbound value Subst.FO.canonize_all_vars
# ocamlc src/prover_phases/.libzipperposition_phases.objs/byte/libzipperposition_phases__Phases_impl.{cmo,cmt} (exit 2)
# (cd _build/default && /home/mbaxwab3/.opam/default/bin/ocamlc.opt -w -40 -warn-error -3 -color always -safe-string -w -32-50 -g -bin-annot -I src/prover_phases/.libzipperposition_phases.objs/byte -I /home/mbaxwab3/.opam/default/lib/bytes -I /home/mbaxwab3/.opam/default/lib/containers -I /home/mbaxwab3/.opam/default/lib/containers/data -I /home/mbaxwab3/.opam/default/lib/containers/monomorphic[...]
# File "src/prover_phases/phases_impl.ml", line 134, characters 27-49:
# 134 | else Iter.flat_map Statement.lift_lambdas)
# ^^^^^^^^^^^^^^^^^^^^^^
# Error: Unbound value Statement.lift_lambdas
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build libzipperposition 1.5
└─
Perhaps someone could indicate where I could download a binary from? It may be easier that way.
2019-11-01 8:22:54 (GMT)
A binary for Linux?
2019-11-01 9:13:14 (GMT)
2019-11-01 9:21:7 (GMT)
Thank you
2019-11-01 16:22:53 (GMT)
I just released 1.5.1 (based on master, so not at all up to date wrt HO reasoning), but hopefully easier to compile with the current set of OCaml packages. It should hit opam in a few hours.
https://github.com/sneeuwballen/zipperposition/releases/tag/1.5.1