Failure to run ./build.sh
Closed this issue · 5 comments
Running Ubuntu 16.04 with OCaml 4.04. The system OCaml compiler is 4.02.3 (i.e., for each new terminal, ocaml -version returns "4.02.3"), but I switched compilers to 4.04 via opam switch 4.04.0 and set the environment accordingly (i.e., ocaml -version returns 4.04.0).
Have installed everything listed here:
https://kind.cs.uiowa.edu/kind2_user_doc/home.html#requirements
autogen.sh seems to run fine, but when I run ./build.sh (I'm fine with default directory), it terminates with the following:
+ /usr/bin/ocamlopt -c -w @P@U@F -I /home/local_user/.opam/4.04.0/lib/biniou -I /home/local_user/.opam/4.04.0/lib/easy-format -I /home/local_user/.opam/4.04.0/lib/yojson -annot -bin-annot -I utils -I c2i -I invgen -I qe -I lustre -I ic3 -I certif -I doc -I smt -I terms -I testgen -I induction -o utils/hString.cmx utils/hString.ml
File "utils/hString.ml", line 224, characters 14-36:
Error: Unbound value String.uppercase_ascii
Command exited with code 2.
Makefile:8: recipe for target 'kind2' failed
make[1]: Leaving directory '/home/local_user/kind2gh/src'
Makefile:39: recipe for target 'kind2' failed
See log attached.
log.txt
Review the setup of your environment, the ./build.sh script is still finding the system version of ocamlopt (/usr/bin/ocamlopt). The first line in your snippet should start with something like:
+ /home/local_user/.opam/4.04.0/bin/ocamlopt.opt -c -w @P@U@F [...]
Curious, my environment reflects 4.04.0 files...
My /usr/bin directory has ocaml version 4.03.2, what would be the repercussions of just copying ~/.opam/4.04.0/bin/ into /usr/bin?
envs.txt
I just installed the 4.04.2 release into /usr {bin,man,lib} to replace the old version. I have switched compilers in opam to 4.04.2 opam switch 4.04.2 and installed all the required packaged (ocamlbuild, ocamlfind, ...). Now ocaml -version and ocamlopt.opt return "4.04.2".
I made some progress in build.sh, but I'm getting hung up in a later segment.
/usr/bin/ocamlopt.opt -I /home/local_user/.opam/4.04.2/lib/biniou -I /home/local_user/.opam/4.04.2/lib/easy-format -I /home/local_user/.opam/4.04.2/lib/yojson /home/local_user/.opam/4.04.2/lib/easy-format/easy_format.cmxa /home/local_user/.opam/4.04.2/lib/biniou/biniou.cmxa /home/local_user/.opam/4.04.2/lib/yojson/yojson.cmxa unix.cmxa str.cmxa nums.cmxa -thread threads.cmxa -I ../../ocamlczmq/lib ZMQ.cmxa kind2Config.cmx version.cmx utils/lib.cmx utils/pretty.cmx log.cmx utils/fileId.cmx flags.cmx debug.cmx terms/hexadecimal.cmx terms/numeral.cmx utils/hashconsStrong.cmx utils/hashconsWeak.cmx utils/hashcons.cmx utils/hString.cmx terms/bitvector.cmx terms/decimal.cmx terms/ltree.cmx terms/type.cmx terms/ufSymbol.cmx terms/stateVar.cmx terms/termAttr.cmx utils/symbol.cmx terms/var.cmx terms/term.cmx actlit.cmx certif/certificate.cmx utils/ident.cmx lustre/lustreAst.cmx utils/scope.cmx lustre/lustreIdent.cmx lustre/lustreExpr.cmx stat.cmx terms/termLib.cmx model.cmx property.cmx terms/invs.cmx transSys.cmx analysis.cmx simplify.cmx terms/eval.cmx c2i/C2ICandidate.cmx lustre/lustreContract.cmx lustre/lustreDependencies.cmx utils/trie.cmx lustre/lustreIndex.cmx strategy.cmx subSystem.cmx lustre/lustreNode.cmx lustre/lustreContext.cmx lustre/lustreGlobals.cmx lustre/lustreParser.cmx lustre/lustreLexer.cmx lustre/lustreSimplify.cmx lustre/lustreDeclarations.cmx lustre/lustreInput.cmx lustre/contractsToProps.cmx lustre/lustrePath.cmx lustre/lustreSlicing.cmx lustre/lustreToRust.cmx lustre/lustreTransSys.cmx smt/solverDriver.cmx utils/SExprBase.cmx utils/hStringSExpr.cmx smt/solverResponse.cmx smt/SMTExpr.cmx smt/genericSMTLIBDriver.cmx utils/SExprParser.cmx utils/SExprLexer.cmx nativeInput.cmx inputSystem.cmx messaging.cmx kEvent.cmx smt/CVC4Driver.cmx smt/SMTLIBSolver.cmx smt/Yices2SMT2Driver.cmx smt/Z3Driver.cmx smt/yicesDriver.cmx smt/yicesResponse.cmx smt/yicesParser.cmx smt/yicesLexer.cmx smt/yicesNative.cmx smt/SMTSolver.cmx utils/unroller.cmx c2i/C2I.cmx c2i/C2Imodel.cmx c2i/C2Icnf.cmx certif/jkindParser.cmx certif/proof.cmx induction/compress.cmx certif/certifChecker.cmx extract.cmx ic3/clause.cmx qe/poly.cmx qe/cooperQE.cmx qe/presburger.cmx qe/QE.cmx ic3/IC3.cmx induction/base.cmx induction/step.cmx induction/step2.cmx inputParser.cmx interpreter.cmx invarManager.cmx invgen/invGenMiner.cmx invgen/invGenDomain.cmx invgen/lockStepDriver.cmx invgen/invGenGraph.cmx invgen/invGen.cmx lustre/lustreContractGen.cmx testgen/testgenIO.cmx testgen/testgenModes.cmx testgen/testgenSolver.cmx testgen/testgenTree.cmx testgen/testgenDF.cmx utils/Res.cmx postAnalysis.cmx kind2Flow.cmx kind2.cmx -o kind2.native
+ /usr/bin/ocamlopt.opt -I /home/local_user/.opam/4.04.2/lib/biniou -I /home/local_user/.opam/4.04.2/lib/easy-format -I /home/local_user/.opam/4.04.2/lib/yojson /home/local_user/.opam/4.04.2/lib/easy-format/easy_format.cmxa /home/local_user/.opam/4.04.2/lib/biniou/biniou.cmxa /home/local_user/.opam/4.04.2/lib/yojson/yojson.cmxa unix.cmxa str.cmxa nums.cmxa -thread threads.cmxa -I ../../ocamlczmq/lib ZMQ.cmxa kind2Config.cmx version.cmx utils/lib.cmx utils/pretty.cmx log.cmx utils/fileId.cmx flags.cmx debug.cmx terms/hexadecimal.cmx terms/numeral.cmx utils/hashconsStrong.cmx utils/hashconsWeak.cmx utils/hashcons.cmx utils/hString.cmx terms/bitvector.cmx terms/decimal.cmx terms/ltree.cmx terms/type.cmx terms/ufSymbol.cmx terms/stateVar.cmx terms/termAttr.cmx utils/symbol.cmx terms/var.cmx terms/term.cmx actlit.cmx certif/certificate.cmx utils/ident.cmx lustre/lustreAst.cmx utils/scope.cmx lustre/lustreIdent.cmx lustre/lustreExpr.cmx stat.cmx terms/termLib.cmx model.cmx property.cmx terms/invs.cmx transSys.cmx analysis.cmx simplify.cmx terms/eval.cmx c2i/C2ICandidate.cmx lustre/lustreContract.cmx lustre/lustreDependencies.cmx utils/trie.cmx lustre/lustreIndex.cmx strategy.cmx subSystem.cmx lustre/lustreNode.cmx lustre/lustreContext.cmx lustre/lustreGlobals.cmx lustre/lustreParser.cmx lustre/lustreLexer.cmx lustre/lustreSimplify.cmx lustre/lustreDeclarations.cmx lustre/lustreInput.cmx lustre/contractsToProps.cmx lustre/lustrePath.cmx lustre/lustreSlicing.cmx lustre/lustreToRust.cmx lustre/lustreTransSys.cmx smt/solverDriver.cmx utils/SExprBase.cmx utils/hStringSExpr.cmx smt/solverResponse.cmx smt/SMTExpr.cmx smt/genericSMTLIBDriver.cmx utils/SExprParser.cmx utils/SExprLexer.cmx nativeInput.cmx inputSystem.cmx messaging.cmx kEvent.cmx smt/CVC4Driver.cmx smt/SMTLIBSolver.cmx smt/Yices2SMT2Driver.cmx smt/Z3Driver.cmx smt/yicesDriver.cmx smt/yicesResponse.cmx smt/yicesParser.cmx smt/yicesLexer.cmx smt/yicesNative.cmx smt/SMTSolver.cmx utils/unroller.cmx c2i/C2I.cmx c2i/C2Imodel.cmx c2i/C2Icnf.cmx certif/jkindParser.cmx certif/proof.cmx induction/compress.cmx certif/certifChecker.cmx extract.cmx ic3/clause.cmx qe/poly.cmx qe/cooperQE.cmx qe/presburger.cmx qe/QE.cmx ic3/IC3.cmx induction/base.cmx induction/step.cmx induction/step2.cmx inputParser.cmx interpreter.cmx invarManager.cmx invgen/invGenMiner.cmx invgen/invGenDomain.cmx invgen/lockStepDriver.cmx invgen/invGenGraph.cmx invgen/invGen.cmx lustre/lustreContractGen.cmx testgen/testgenIO.cmx testgen/testgenModes.cmx testgen/testgenSolver.cmx testgen/testgenTree.cmx testgen/testgenDF.cmx utils/Res.cmx postAnalysis.cmx kind2Flow.cmx kind2.cmx -o kind2.native
File "_none_", line 1:
Error: Files ../../ocamlczmq/lib/ZMQ.cmxa and /usr/lib/ocaml/stdlib.cmxa
make inconsistent assumptions over implementation Gc
Command exited with code 2.
Makefile:8: recipe for target 'kind2' failed
make[1]: Leaving directory '/home/local_user/kind2gh/src'
Makefile:39: recipe for target 'kind2' failed
I can see that it still has that reference to /usr/bin/ocamlopt.opt instead of /home/local_user/.opam/4.04.2/bin/ocamlopt.opt`. I'm not sure how to change that, and I'm not sure if that's the problem, since both files are of the same version.
It is possible that you are getting that error because some .cmxa files were compiled with the old version. Run make clean and try to build the system again.
Fixed. Thanks!