Hey,
I'm trying to build VPLTactic from source. I'm building it on the special vagrant box that was issued, but it doesn't work.
I'm using the vagrant setup described on opam-vpl.
make traceback
make -j -f tactic.mk src/vpltactics.cmx "OPT:=-opt" "CAMLC:=ocamlfind ocamlc -c -rectypes -thread -package vpl -linkpkg" "CAMLOPTC:=ocamlfind ocamlopt -c -rectypes -thread -package vpl -linkpkg" "CAMLLINK:=ocamlfind ocamlc -rectypes -thread -package vpl -linkpkg" "CAMLOPTLINK:=ocamlfind ocamlopt -rectypes -thread -package vpl -linkpkg"
make[1]: Entering directory '/home/ubuntu/work/VplTactic'
CAMLDEP src/reification.mli
COQDEP src/vpl_plugin.mllib
CAMLDEP src/reification.ml
COQDEP test-suite/Demo.v
COQDEP test-suite/Test.v
COQDEP theories/Tactic.v
COQDEP theories/Reduction.v
COQDEP theories/Input.v
*** Warning: vpl_plugin.mllib already found in src (discarding src/vpl_plugin.mllib)
COQDEP theories/Output.v
CAMLDEP -pp src/vpltactics.ml4
COQDEP test-suite/Examples.v
CAMLC -c src/reification.mli
File "src/reification.mli", line 19, characters 45-59:
Error: Unbound module EConstr
Hint: Did you mean Cstr or Cons?
tactic.mk:432: recipe for target 'src/reification.cmi' failed
make[1]: *** [src/reification.cmi] Error 2
make[1]: Leaving directory '/home/ubuntu/work/VplTactic'
Makefile:11: recipe for target 'tactic' failed
make: *** [tactic] Error 2
Hey,
I'm trying to build VPLTactic from source. I'm building it on the special vagrant box that was issued, but it doesn't work.
I'm using the vagrant setup described on
opam-vpl.maketraceback