EHRL Proof checker build error - Atdgen-runtime unbound module
Closed this issue · 1 comments
I have built llvm and vellvm but am having difficulty with building the proof checker the error I am experiencing is shown below:
File "corehint/coreHint_j.ml", line 2332, characters 14-55:
Error: Unbound module Atdgen_runtime
Command exited with code 2.
Compilation unsuccessful after building 391 targets (390 cached) in 00:00:00.
Makefile:32: recipe for target 'main.native' failed
make[1]: *** [main.native] Error 10
make[1]: Leaving directory '/home/tpottei1/crellvm/crellvm/ocaml'
Makefile:74: recipe for target 'exec' failed
make: *** [exec] Error 2
I installed atdgen-runtime with the command opam install atdgen-runtime but am still experiencing this issue. What could be the root cause?
Modified OCAMLBUILD_OPT in the Makefile inside of ocaml directory. Make exec successfully executes.
Changed line -use-ocamlfind -pkg atdgen
to -use-ocamlfind -pkg atdgen-runtime -pkg atdgen