Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Installation error #12

Closed
alxest opened this issue Apr 5, 2015 · 6 comments
Closed

Installation error #12

alxest opened this issue Apr 5, 2015 · 6 comments

Comments

@alxest
Copy link

alxest commented Apr 5, 2015

I followed installing steps, and encountered following error.

~/vellvm-legacy $ ./scripts/fetch-libs.sh 
Downloading ./src/Coq-Equations-8.4.zip ... archive exists, skipping
Extracting to Coq-Equations-8.4 ... target dir exists, skipping
Downloading ./src/metalib-20090714.zip ... archive exists, skipping
Extracting to metalib-20090714 ... target dir exists, skipping
Downloading ./src/cpdtlib.tgz ... archive exists, skipping
Extracting to cpdtlib ... target dir exists, skipping
Downloading ./src/GraphBasics.tgz ... archive exists, skipping
Extracting to GraphBasics ... target dir exists, skipping
Downloading ./src/compcert-1.9.tgz ... archive exists, skipping
Extracting to compcert-1.9 ... target dir exists, skipping
Done!
~/vellvm-legacy $ make libs
make -C lib/Coq-Equations-8.4
make[1]: Entering directory `/home/youngju.song/vellvm-legacy/lib/Coq-Equations-8.4'
ocamlc -c -rectypes  -I src -I /home/youngju.song/.opam/4.02.1/lib/coq/kernel -I /home/youngju.song/.opam/4.02.1/lib/coq/lib -I /home/youngju.song/.opam/4.02.1/lib/coq/library -I /home/youngju.song/.opam/4.02.1/lib/coq/parsing -I /home/youngju.song/.opam/4.02.1/lib/coq/pretyping -I /home/youngju.song/.opam/4.02.1/lib/coq/interp -I /home/youngju.song/.opam/4.02.1/lib/coq/proofs -I /home/youngju.song/.opam/4.02.1/lib/coq/tactics -I /home/youngju.song/.opam/4.02.1/lib/coq/toplevel -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/cc -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/decl_mode -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/extraction -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/field -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/firstorder -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/fourier -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/funind -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/micromega -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/nsatz -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/omega -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/quote -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/ring -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/romega -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/rtauto -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/setoid_ring -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/subtac -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/subtac/test -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/syntax -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/xml -I /home/youngju.song/.opam/4.02.1/lib/camlp5 -pp "/home/youngju.song/.opam/4.02.1/bin/camlp5o -I /home/youngju.song/.opam/4.02.1/lib/ocaml/ -I . -I /home/youngju.song/.opam/4.02.1/lib/coq/kernel -I /home/youngju.song/.opam/4.02.1/lib/coq/lib -I /home/youngju.song/.opam/4.02.1/lib/coq/library -I /home/youngju.song/.opam/4.02.1/lib/coq/parsing -I /home/youngju.song/.opam/4.02.1/lib/coq/pretyping -I /home/youngju.song/.opam/4.02.1/lib/coq/interp -I /home/youngju.song/.opam/4.02.1/lib/coq/proofs -I /home/youngju.song/.opam/4.02.1/lib/coq/tactics -I /home/youngju.song/.opam/4.02.1/lib/coq/toplevel -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/cc -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/decl_mode -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/extraction -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/field -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/firstorder -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/fourier -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/funind -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/micromega -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/nsatz -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/omega -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/quote -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/ring -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/romega -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/rtauto -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/setoid_ring -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/subtac -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/subtac/test -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/syntax -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/xml pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl" -impl src/equations.ml4
File "src/equations.ml4", line 2814, characters 3-9:
Parse error: ':' expected after [name] (in [entry])
File "src/equations.ml4", line 1:
Error: Error while running external preprocessor
Command line: /home/youngju.song/.opam/4.02.1/bin/camlp5o -I /home/youngju.song/.opam/4.02.1/lib/ocaml/ -I . -I /home/youngju.song/.opam/4.02.1/lib/coq/kernel -I /home/youngju.song/.opam/4.02.1/lib/coq/lib -I /home/youngju.song/.opam/4.02.1/lib/coq/library -I /home/youngju.song/.opam/4.02.1/lib/coq/parsing -I /home/youngju.song/.opam/4.02.1/lib/coq/pretyping -I /home/youngju.song/.opam/4.02.1/lib/coq/interp -I /home/youngju.song/.opam/4.02.1/lib/coq/proofs -I /home/youngju.song/.opam/4.02.1/lib/coq/tactics -I /home/youngju.song/.opam/4.02.1/lib/coq/toplevel -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/cc -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/decl_mode -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/extraction -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/field -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/firstorder -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/fourier -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/funind -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/micromega -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/nsatz -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/omega -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/quote -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/ring -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/romega -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/rtauto -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/setoid_ring -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/subtac -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/subtac/test -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/syntax -I /home/youngju.song/.opam/4.02.1/lib/coq/plugins/xml pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl 'src/equations.ml4' > /tmp/ocamlpp96c0c5

make[1]: *** [src/equations.cmo] Error 2
make[1]: Leaving directory `/home/youngju.song/vellvm-legacy/lib/Coq-Equations-8.4'
make: *** [libs] Error 2

My coqc version is:

~/vellvm-legacy $ coqc -v
The Coq Proof Assistant, version 8.4pl5 (March 2015)
compiled on Mar 22 2015 21:39:14 with OCaml 4.02.1

and ocaml version is:

~/vellvm-legacy $ ocaml -version
The OCaml toplevel, version 4.02.1

ott version is:

Ott version 0.25   distribution of Thu Sep 4 18:04:34 BST 2014

camlp4 version is:

~/ott_distro_0.24 $ camlp4 -v
Camlp4 version 4.02.1

So, the question is:

  1. It is written that "Coq 8.4pl4, configured with -usecamlp4 option", how can I configure coq with that option?
  2. I have tried to install ott version 0.24. I've found Opam offers ott package but I haven't found how to install specific version of it. Therefore, I have downloaded from here (http://www.cl.cam.ac.uk/~pes20/ott/ott_distro_0.24.tar.gz) and tried to install it. I failed and below is message:
~/ott_distro_0.24 $ make
cd src; /usr/bin/make install
make[1]: Entering directory `/home/youngju.song/ott_distro_0.24/src'
cd .. && tar -zxvf ocamlgraph-1.7.tar.gz
ocamlgraph-1.7/
ocamlgraph-1.7/bin/
ocamlgraph-1.7/src/
ocamlgraph-1.7/src/blocks.ml
ocamlgraph-1.7/src/builder.ml
ocamlgraph-1.7/src/builder.mli
ocamlgraph-1.7/src/classic.ml
ocamlgraph-1.7/src/classic.mli
ocamlgraph-1.7/src/cliquetree.ml
ocamlgraph-1.7/src/cliquetree.mli
ocamlgraph-1.7/src/coloring.ml
ocamlgraph-1.7/src/coloring.mli
ocamlgraph-1.7/src/components.ml
ocamlgraph-1.7/src/components.mli
ocamlgraph-1.7/src/delaunay.ml
ocamlgraph-1.7/src/delaunay.mli
ocamlgraph-1.7/src/dot.ml
ocamlgraph-1.7/src/dot.mli
ocamlgraph-1.7/src/dot_ast.mli
ocamlgraph-1.7/src/dot_lexer.ml
ocamlgraph-1.7/src/dot_lexer.mll
ocamlgraph-1.7/src/dot_parser.ml
ocamlgraph-1.7/src/dot_parser.mli
ocamlgraph-1.7/src/dot_parser.mly
ocamlgraph-1.7/src/flow.ml
ocamlgraph-1.7/src/flow.mli
ocamlgraph-1.7/src/gmap.ml
ocamlgraph-1.7/src/gmap.mli
ocamlgraph-1.7/src/gml.ml
ocamlgraph-1.7/src/gml.mli
ocamlgraph-1.7/src/gml.mll
ocamlgraph-1.7/src/graphviz.ml
ocamlgraph-1.7/src/graphviz.mli
ocamlgraph-1.7/src/imperative.ml
ocamlgraph-1.7/src/imperative.mli
ocamlgraph-1.7/src/kruskal.ml
ocamlgraph-1.7/src/kruskal.mli
ocamlgraph-1.7/src/mcs_m.ml
ocamlgraph-1.7/src/mcs_m.mli
ocamlgraph-1.7/src/md.ml
ocamlgraph-1.7/src/md.mli
ocamlgraph-1.7/src/minsep.ml
ocamlgraph-1.7/src/minsep.mli
ocamlgraph-1.7/src/oper.ml
ocamlgraph-1.7/src/oper.mli
ocamlgraph-1.7/src/pack.ml
ocamlgraph-1.7/src/pack.mli
ocamlgraph-1.7/src/path.ml
ocamlgraph-1.7/src/path.mli
ocamlgraph-1.7/src/persistent.ml
ocamlgraph-1.7/src/persistent.mli
ocamlgraph-1.7/src/rand.ml
ocamlgraph-1.7/src/rand.mli
ocamlgraph-1.7/src/sig.mli
ocamlgraph-1.7/src/sig_pack.mli
ocamlgraph-1.7/src/strat.ml
ocamlgraph-1.7/src/strat.mli
ocamlgraph-1.7/src/topological.ml
ocamlgraph-1.7/src/topological.mli
ocamlgraph-1.7/src/traverse.ml
ocamlgraph-1.7/src/traverse.mli
ocamlgraph-1.7/src/util.ml
ocamlgraph-1.7/src/util.mli
ocamlgraph-1.7/src/version.ml
ocamlgraph-1.7/lib/
ocamlgraph-1.7/lib/bitv.ml
ocamlgraph-1.7/lib/bitv.mli
ocamlgraph-1.7/lib/heap.ml
ocamlgraph-1.7/lib/heap.mli
ocamlgraph-1.7/lib/unionfind.ml
ocamlgraph-1.7/lib/unionfind.mli
ocamlgraph-1.7/Makefile.in
ocamlgraph-1.7/configure
ocamlgraph-1.7/configure.in
ocamlgraph-1.7/META.in
ocamlgraph-1.7/.depend
ocamlgraph-1.7/editor/
ocamlgraph-1.7/editor/ed_display.ml
ocamlgraph-1.7/editor/ed_draw.ml
ocamlgraph-1.7/editor/ed_graph.ml
ocamlgraph-1.7/editor/ed_hyper.ml
ocamlgraph-1.7/editor/ed_main.ml
ocamlgraph-1.7/editor/Makefile
ocamlgraph-1.7/editor/tests/
ocamlgraph-1.7/editor/tests/dep_ed.dot
ocamlgraph-1.7/editor/tests/dep_why.dot
ocamlgraph-1.7/editor/tests/fsm.dot
ocamlgraph-1.7/editor/tests/parcours.dot
ocamlgraph-1.7/editor/tests/softmaint.dot
ocamlgraph-1.7/editor/tests/transparency.dot
ocamlgraph-1.7/editor/tests/twopi2.dot
ocamlgraph-1.7/editor/tests/unix.dot
ocamlgraph-1.7/editor/tests/world.dot
ocamlgraph-1.7/editor/tests/de_bruijn4.gml
ocamlgraph-1.7/editor/tests/divisors12.gml
ocamlgraph-1.7/editor/tests/full10.gml
ocamlgraph-1.7/editor/tests/full20.gml
ocamlgraph-1.7/editor/tests/full30.gml
ocamlgraph-1.7/editor/tests/full50.gml
ocamlgraph-1.7/editor/tests/rand_100_10.gml
ocamlgraph-1.7/editor/tests/rand_100_300.gml
ocamlgraph-1.7/editor/tests/rand_10_10.gml
ocamlgraph-1.7/editor/tests/rand_10_40.gml
ocamlgraph-1.7/editor/tests/rand_50_300.gml
ocamlgraph-1.7/editor/tests/ring_100.gml
ocamlgraph-1.7/editor/tests/test.gml
ocamlgraph-1.7/editor/tests/test2,1_2.gml
ocamlgraph-1.7/editor/tests/test2,1_3.gml
ocamlgraph-1.7/editor/tests/test2,1_3tot.gml
ocamlgraph-1.7/editor/tests/test2_2.gml
ocamlgraph-1.7/view_graph/
ocamlgraph-1.7/view_graph/viewGraph_core.ml
ocamlgraph-1.7/view_graph/viewGraph_select.ml
ocamlgraph-1.7/view_graph/viewGraph_test.ml
ocamlgraph-1.7/view_graph/viewGraph_utils.ml
ocamlgraph-1.7/view_graph/viewGraph_core.mli
ocamlgraph-1.7/view_graph/viewGraph_select.mli
ocamlgraph-1.7/view_graph/viewGraph_utils.mli
ocamlgraph-1.7/view_graph/README
ocamlgraph-1.7/view_graph/Makefile
ocamlgraph-1.7/dgraph/
ocamlgraph-1.7/dgraph/dGraphContainer.ml
ocamlgraph-1.7/dgraph/dGraphMake.ml
ocamlgraph-1.7/dgraph/dGraphModel.ml
ocamlgraph-1.7/dgraph/dGraphRandModel.ml
ocamlgraph-1.7/dgraph/dGraphSubTree.ml
ocamlgraph-1.7/dgraph/dGraphTreeLayout.ml
ocamlgraph-1.7/dgraph/dGraphTreeModel.ml
ocamlgraph-1.7/dgraph/dGraphView.ml
ocamlgraph-1.7/dgraph/dGraphViewItem.ml
ocamlgraph-1.7/dgraph/dGraphViewer.ml
ocamlgraph-1.7/dgraph/xDot.ml
ocamlgraph-1.7/dgraph/xDotDraw.ml
ocamlgraph-1.7/dgraph/dGraphContainer.mli
ocamlgraph-1.7/dgraph/dGraphModel.mli
ocamlgraph-1.7/dgraph/dGraphRandModel.mli
ocamlgraph-1.7/dgraph/dGraphSubTree.mli
ocamlgraph-1.7/dgraph/dGraphTreeLayout.mli
ocamlgraph-1.7/dgraph/dGraphTreeModel.mli
ocamlgraph-1.7/dgraph/dGraphView.mli
ocamlgraph-1.7/dgraph/dGraphViewItem.mli
ocamlgraph-1.7/dgraph/xDot.mli
ocamlgraph-1.7/dgraph/xDotDraw.mli
ocamlgraph-1.7/examples/
ocamlgraph-1.7/examples/color.ml
ocamlgraph-1.7/examples/demo.ml
ocamlgraph-1.7/examples/demo_planar.ml
ocamlgraph-1.7/examples/sudoku.ml
ocamlgraph-1.7/tests/
ocamlgraph-1.7/tests/bench.ml
ocamlgraph-1.7/tests/check.ml
ocamlgraph-1.7/tests/dot.ml
ocamlgraph-1.7/tests/strat.ml
ocamlgraph-1.7/tests/test.ml
ocamlgraph-1.7/README
ocamlgraph-1.7/FAQ
ocamlgraph-1.7/CREDITS
ocamlgraph-1.7/INSTALL
ocamlgraph-1.7/COPYING
ocamlgraph-1.7/LICENSE
ocamlgraph-1.7/CHANGES
cd ../ocamlgraph-1.7 && ./configure
checking for ocamlc... ocamlc
ocaml version is 4.02.1
ocaml library path is /home/youngju.song/.opam/4.02.1/lib/ocaml
checking for ocamlopt... ocamlopt
checking ocamlopt version... ok
checking for ocamlc.opt... ocamlc.opt
checking ocamlc.opt version... ok
checking for ocamlopt.opt... ocamlopt.opt
checking ocamlc.opt version... ok
checking for ocamldep... ocamldep
checking for ocamllex... ocamllex
checking for ocamllex.opt... ocamllex.opt
checking for ocamlyacc... ocamlyacc
checking for ocamldoc... ocamldoc
checking for ocamldoc.opt... ocamldoc.opt
checking for ocamlweb... true
checking for ocamlfind... ocamlfind
checking for /home/youngju.song/.opam/4.02.1/lib/ocaml/lablgtk2/lablgtk.cmxa... no
checking Win32 platform... no
configure: WARNING: lablgnomecanvas not found: the graph editor and view_graph will not be compiled
configure: creating ./config.status
config.status: creating Makefile
cd ../ocamlgraph-1.7 && \
/usr/bin/make OCAMLOPT='ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib' graph.cmxa
make[2]: Entering directory `/home/youngju.song/ott_distro_0.24/ocamlgraph-1.7'
sed -e s/VERSION/1.7/ -e s/CMA/graph.cma/ -e s/CMXA/graph.cmxa/ \
    META.in > META
rm -f src/version.ml
echo "let version = \""1.7"\"" > src/version.ml
echo "let date = \""`date`"\"" >> src/version.ml
rm -f .depend
ocamldep -slash -I src -I lib -I editor -I view_graph -I dgraph\
    lib/*.ml lib/*.mli \
    src/*.ml src/*.mli \
    editor/*.mli editor/*.ml \
    view_graph/*.mli view_graph/*.ml \
    dgraph/*.mli dgraph/*.ml > .depend
make[2]: Leaving directory `/home/youngju.song/ott_distro_0.24/ocamlgraph-1.7'
make[2]: Entering directory `/home/youngju.song/ott_distro_0.24/ocamlgraph-1.7'
ocamlc.opt -c -I src -I lib -g -dtypes src/sig.mli
ocamlc.opt -c -I src -I lib -g -dtypes src/sig_pack.mli
ocamlc.opt -c -I src -I lib -g -dtypes src/dot_ast.mli
ocamlc.opt -c -I src -I lib -g -dtypes lib/unionfind.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph lib/unionfind.ml
ocamlc.opt -c -I src -I lib -g -dtypes lib/heap.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph lib/heap.ml
File "lib/heap.ml", line 54, characters 13-25:
Warning 3: deprecated: Array.create
Use Array.make instead.
File "lib/heap.ml", line 61, characters 16-28:
Warning 3: deprecated: Array.create
Use Array.make instead.
ocamlc.opt -c -I src -I lib -g -dtypes lib/bitv.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph lib/bitv.ml
File "lib/bitv.ml", line 51, characters 15-27:
Warning 3: deprecated: Array.create
Use Array.make instead.
File "lib/bitv.ml", line 68, characters 25-37:
Warning 3: deprecated: Array.create
Use Array.make instead.
File "lib/bitv.ml", line 71, characters 12-24:
Warning 3: deprecated: Array.create
Use Array.make instead.
File "lib/bitv.ml", line 113, characters 11-13:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "lib/bitv.ml", line 118, characters 11-13:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "lib/bitv.ml", line 205, characters 13-15:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "lib/bitv.ml", line 205, characters 25-27:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "lib/bitv.ml", line 206, characters 13-15:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "lib/bitv.ml", line 206, characters 25-27:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "lib/bitv.ml", line 214, characters 13-15:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "lib/bitv.ml", line 214, characters 24-26:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "lib/bitv.ml", line 289, characters 13-15:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "lib/bitv.ml", line 289, characters 24-26:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "lib/bitv.ml", line 368, characters 10-22:
Warning 3: deprecated: Array.create
Use Array.make instead.
File "lib/bitv.ml", line 380, characters 10-22:
Warning 3: deprecated: Array.create
Use Array.make instead.
File "lib/bitv.ml", line 392, characters 10-22:
Warning 3: deprecated: Array.create
Use Array.make instead.
File "lib/bitv.ml", line 401, characters 10-22:
Warning 3: deprecated: Array.create
Use Array.make instead.
File "lib/bitv.ml", line 464, characters 27-39:
Warning 3: deprecated: String.unsafe_set
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/version.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/util.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/util.ml
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/blocks.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/persistent.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/persistent.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/imperative.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/imperative.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/delaunay.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/delaunay.ml
File "src/delaunay.ml", line 260, characters 19-31:
Warning 3: deprecated: Array.create
Use Array.make instead.
ocamlc.opt -c -I src -I lib -g -dtypes src/builder.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/builder.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/classic.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/classic.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/rand.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/rand.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/oper.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/oper.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/path.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/path.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/traverse.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/traverse.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/coloring.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/coloring.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/topological.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/topological.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/components.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/components.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/kruskal.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/kruskal.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/flow.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/flow.ml
File "src/flow.ml", line 53, characters 54-56:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "src/flow.ml", line 137, characters 6-8:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "src/flow.ml", line 136, characters 44-46:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "src/flow.ml", line 137, characters 47-49:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
File "src/flow.ml", line 141, characters 40-42:
Warning 3: deprecated: Pervasives.or
Use (||) instead.
ocamlc.opt -c -I src -I lib -g -dtypes src/graphviz.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/graphviz.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/gml.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/gml.ml
File "src/gml.ml", line 418, characters 27-39:
Warning 3: deprecated: Array.create
Use Array.make instead.
File "src/gml.ml", line 455, characters 27-39:
Warning 3: deprecated: Array.create
Use Array.make instead.
ocamlc.opt -c -I src -I lib -g -dtypes src/dot_parser.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/dot_parser.ml
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/dot_lexer.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/dot.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/dot.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/pack.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/pack.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/gmap.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/gmap.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/minsep.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/minsep.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/cliquetree.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/cliquetree.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/mcs_m.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/mcs_m.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/md.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/md.ml
ocamlc.opt -c -I src -I lib -g -dtypes src/strat.mli
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/strat.ml
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -I src -I lib -pack -o graph.cmx src/sig.cmi src/sig_pack.cmi src/dot_ast.cmi lib/unionfind.cmx lib/heap.cmx lib/bitv.cmx src/version.cmx src/util.cmx src/blocks.cmx src/persistent.cmx src/imperative.cmx src/delaunay.cmx src/builder.cmx src/classic.cmx src/rand.cmx src/oper.cmx src/path.cmx src/traverse.cmx src/coloring.cmx src/topological.cmx src/components.cmx src/kruskal.cmx src/flow.cmx src/graphviz.cmx src/gml.cmx src/dot_parser.cmx src/dot_lexer.cmx src/dot.cmx src/pack.cmx src/gmap.cmx src/minsep.cmx src/cliquetree.cmx src/mcs_m.cmx src/md.cmx src/strat.cmx
ocamlopt -w p -w y -unsafe -inline 9 -I src -I lib -I src -I lib -a -o graph.cmxa graph.cmx
make[2]: Leaving directory `/home/youngju.song/ott_distro_0.24/ocamlgraph-1.7'
/usr/bin/make opt
make[2]: Entering directory `/home/youngju.song/ott_distro_0.24/src'
ocamlopt -w p -w y -unsafe -inline 9 -I ../ocamlgraph-1.7 -c location.ml
ocamlopt -w p -w y -unsafe -inline 9 -I ../ocamlgraph-1.7 -c types.ml
ocamlopt -w p -w y -unsafe -inline 9 -I ../ocamlgraph-1.7 -c auxl.ml
File "auxl.ml", line 196, characters 10-23:
Warning 3: deprecated: String.create
Use Bytes.create instead.
File "auxl.ml", line 200, characters 15-25:
Warning 3: deprecated: String.set
Use Bytes.set instead.
File "auxl.ml", line 1834, characters 13-26:
Warning 3: deprecated: String.create
Use Bytes.create instead.
ocamlc -g -w p -w y  -c location.ml
ocamlc -g -w p -w y  -c types.ml
ocamlc -g -w p -w y  -I ../ocamlgraph-1.7 -c merge.mli
ocamlopt -w p -w y -unsafe -inline 9 -I ../ocamlgraph-1.7 -c merge.ml
ocamlopt -w p -w y -unsafe -inline 9 -I ../ocamlgraph-1.7 -c global_option.ml
ocamlc -g -w p -w y  -I ../ocamlgraph-1.7 -c grammar_parser.mli
ocamlopt -w p -w y -unsafe -inline 9 -I ../ocamlgraph-1.7 -c grammar_parser.ml
ocamlopt -w p -w y -unsafe -inline 9 -I ../ocamlgraph-1.7 -c grammar_lexer.ml
ocamlopt -w p -w y -unsafe -inline 9 -I ../ocamlgraph-1.7 -c version.ml
ocamlopt -w p -w y -unsafe -inline 9 -I ../ocamlgraph-1.7 -c grammar_pp.ml
File "grammar_pp.ml", line 2706, characters 22-23:
Warning 3: deprecated: Pervasives.&
Use (&&) instead.
ocamlopt -w p -w y -unsafe -inline 9 -c -I ../ocamlgraph-1.7 parse_table.ml
ocamlopt -w p -w y -unsafe -inline 9 -c -I ../ocamlgraph-1.7 glr.ml
ocamlopt -w p -w y -unsafe -inline 9 -c -I ../ocamlgraph-1.7 new_term_parser.ml
ocamlc -g -w p -w y  -I ../ocamlgraph-1.7 -c term_parser.mli
ocamlopt -w p -w y -unsafe -inline 9 -I ../ocamlgraph-1.7 -c term_parser.ml
ocamlc -g -w p -w y  -I ../ocamlgraph-1.7 -c dependency.mli
ocamlopt -w p -w y -unsafe -inline 9 -c -I ../ocamlgraph-1.7 dependency.ml
ocamlc -g -w p -w y  -I ../ocamlgraph-1.7 -c bounds.mli
ocamlopt -w p -w y -unsafe -inline 9 -I ../ocamlgraph-1.7 -c bounds.ml
ocamlopt -w p -w y -unsafe -inline 9 -I ../ocamlgraph-1.7 -c context_pp.ml
ocamlc -g -w p -w y  -I ../ocamlgraph-1.7 -c grammar_typecheck.mli
ocamlopt -w p -w y -unsafe -inline 9 -c -I ../ocamlgraph-1.7 grammar_typecheck.ml
File "grammar_typecheck.ml", line 59, characters 0-2:
Error: This comment contains an unterminated string literal
File "grammar_typecheck.ml", line 89, characters 20-26:
Error: String literal begins here
make[2]: *** [grammar_typecheck.cmx] Error 2
make[2]: Leaving directory `/home/youngju.song/ott_distro_0.24/src'
make[1]: *** [install] Error 2
make[1]: Leaving directory `/home/youngju.song/ott_distro_0.24/src'
make: *** [world] Error 2

~/ott_distro_0.24 $ make world
cd src; /usr/bin/make install
make[1]: Entering directory `/home/youngju.song/ott_distro_0.24/src'
/usr/bin/make opt
make[2]: Entering directory `/home/youngju.song/ott_distro_0.24/src'
ocamlopt -w p -w y -unsafe -inline 9 -c -I ../ocamlgraph-1.7 grammar_typecheck.ml
File "grammar_typecheck.ml", line 59, characters 0-2:
Error: This comment contains an unterminated string literal
File "grammar_typecheck.ml", line 89, characters 20-26:
Error: String literal begins here
make[2]: *** [grammar_typecheck.cmx] Error 2
make[2]: Leaving directory `/home/youngju.song/ott_distro_0.24/src'
make[1]: *** [install] Error 2
make[1]: Leaving directory `/home/youngju.song/ott_distro_0.24/src'
make: *** [world] Error 2

Now I'm stuck. Can you suggest me how to deal with this?
Any comments are welcome.
Thank you.
@jeehoonkang
Copy link
Contributor

I guess the problem lies on the configuration. Coq should be configured with --usecamlp4 option.

Jeehoon

@alxest
Copy link
Author

alxest commented Apr 5, 2015

@jeehoonkang
Actually, that was my first question. Would you explain me how to config coq with that option?

@alxest
Copy link
Author

alxest commented Apr 5, 2015

Following @jeehoonkang 's advice, I rebuilt coq with -usecamlp4 option.
Here is new error message.

[youngju.song@yoda]~/vellvm-legacy% make libs
make -C lib/Coq-Equations-8.4
make[1]: Entering directory `/home/youngju.song/vellvm-legacy/lib/Coq-Equations-8.4'
ocamlc.opt -c -rectypes  -I src -I /home/youngju.song/.local/lib/coq/kernel -I /home/youngju.song/.local/lib/coq/lib -I /home/youngju.song/.local/lib/co
q/library -I /home/youngju.song/.local/lib/coq/parsing -I /home/youngju.song/.local/lib/coq/pretyping -I /home/youngju.song/.local/lib/coq/interp -I /ho
me/youngju.song/.local/lib/coq/proofs -I /home/youngju.song/.local/lib/coq/tactics -I /home/youngju.song/.local/lib/coq/toplevel -I /home/youngju.song/.
local/lib/coq/plugins/cc -I /home/youngju.song/.local/lib/coq/plugins/decl_mode -I /home/youngju.song/.local/lib/coq/plugins/extraction -I /home/youngju
.song/.local/lib/coq/plugins/field -I /home/youngju.song/.local/lib/coq/plugins/firstorder -I /home/youngju.song/.local/lib/coq/plugins/fourier -I /home
/youngju.song/.local/lib/coq/plugins/funind -I /home/youngju.song/.local/lib/coq/plugins/micromega -I /home/youngju.song/.local/lib/coq/plugins/nsatz -I
 /home/youngju.song/.local/lib/coq/plugins/omega -I /home/youngju.song/.local/lib/coq/plugins/quote -I /home/youngju.song/.local/lib/coq/plugins/ring -I
 /home/youngju.song/.local/lib/coq/plugins/romega -I /home/youngju.song/.local/lib/coq/plugins/rtauto -I /home/youngju.song/.local/lib/coq/plugins/setoi
d_ring -I /home/youngju.song/.local/lib/coq/plugins/subtac -I /home/youngju.song/.local/lib/coq/plugins/subtac/test -I /home/youngju.song/.local/lib/coq
/plugins/syntax -I /home/youngju.song/.local/lib/coq/plugins/xml -I /home/youngju.song/.opam/4.02.1/lib/ocaml/camlp4 -pp "/home/youngju.song/.opam/4.02.
1/bin/camlp4o -I /home/youngju.song/.opam/4.02.1/lib/ocaml/ -I . -I /home/youngju.song/.local/lib/coq/kernel -I /home/youngju.song/.local/lib/coq/lib -I
 /home/youngju.song/.local/lib/coq/library -I /home/youngju.song/.local/lib/coq/parsing -I /home/youngju.song/.local/lib/coq/pretyping -I /home/youngju.
song/.local/lib/coq/interp -I /home/youngju.song/.local/lib/coq/proofs -I /home/youngju.song/.local/lib/coq/tactics -I /home/youngju.song/.local/lib/coq
/toplevel -I /home/youngju.song/.local/lib/coq/plugins/cc -I /home/youngju.song/.local/lib/coq/plugins/decl_mode -I /home/youngju.song/.local/lib/coq/pl
ugins/extraction -I /home/youngju.song/.local/lib/coq/plugins/field -I /home/youngju.song/.local/lib/coq/plugins/firstorder -I /home/youngju.song/.local
/lib/coq/plugins/fourier -I /home/youngju.song/.local/lib/coq/plugins/funind -I /home/youngju.song/.local/lib/coq/plugins/micromega -I /home/youngju.son
g/.local/lib/coq/plugins/nsatz -I /home/youngju.song/.local/lib/coq/plugins/omega -I /home/youngju.song/.local/lib/coq/plugins/quote -I /home/youngju.so
ng/.local/lib/coq/plugins/ring -I /home/youngju.song/.local/lib/coq/plugins/romega -I /home/youngju.song/.local/lib/coq/plugins/rtauto -I /home/youngju.
song/.local/lib/coq/plugins/setoid_ring -I /home/youngju.song/.local/lib/coq/plugins/subtac -I /home/youngju.song/.local/lib/coq/plugins/subtac/test -I 
/home/youngju.song/.local/lib/coq/plugins/syntax -I /home/youngju.song/.local/lib/coq/plugins/xml pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -lo
c loc -impl" -impl src/equations_common.ml4                                                                                                            
Camlp4: Uncaught exception: DynLoader.Error ("grammar.cma", "file not found in path")

File "src/equations_common.ml4", line 1:
Error: Error while running external preprocessor
Command line: /home/youngju.song/.opam/4.02.1/bin/camlp4o -I /home/youngju.song/.opam/4.02.1/lib/ocaml/ -I . -I /home/youngju.song/.local/lib/coq/kernel
 -I /home/youngju.song/.local/lib/coq/lib -I /home/youngju.song/.local/lib/coq/library -I /home/youngju.song/.local/lib/coq/parsing -I /home/youngju.son
g/.local/lib/coq/pretyping -I /home/youngju.song/.local/lib/coq/interp -I /home/youngju.song/.local/lib/coq/proofs -I /home/youngju.song/.local/lib/coq/
tactics -I /home/youngju.song/.local/lib/coq/toplevel -I /home/youngju.song/.local/lib/coq/plugins/cc -I /home/youngju.song/.local/lib/coq/plugins/decl_
mode -I /home/youngju.song/.local/lib/coq/plugins/extraction -I /home/youngju.song/.local/lib/coq/plugins/field -I /home/youngju.song/.local/lib/coq/plu
gins/firstorder -I /home/youngju.song/.local/lib/coq/plugins/fourier -I /home/youngju.song/.local/lib/coq/plugins/funind -I /home/youngju.song/.local/li
b/coq/plugins/micromega -I /home/youngju.song/.local/lib/coq/plugins/nsatz -I /home/youngju.song/.local/lib/coq/plugins/omega -I /home/youngju.song/.loc
al/lib/coq/plugins/quote -I /home/youngju.song/.local/lib/coq/plugins/ring -I /home/youngju.song/.local/lib/coq/plugins/romega -I /home/youngju.song/.lo
cal/lib/coq/plugins/rtauto -I /home/youngju.song/.local/lib/coq/plugins/setoid_ring -I /home/youngju.song/.local/lib/coq/plugins/subtac -I /home/youngju
.song/.local/lib/coq/plugins/subtac/test -I /home/youngju.song/.local/lib/coq/plugins/syntax -I /home/youngju.song/.local/lib/coq/plugins/xml pa_extend.
cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl 'src/equations_common.ml4' > /tmp/ocamlpp2713c7                                                

make[1]: *** [src/equations_common.cmo] Error 2
make[1]: Leaving directory `/home/youngju.song/vellvm-legacy/lib/Coq-Equations-8.4'
make: *** [libs] Error 2

@alxest
Copy link
Author

alxest commented Apr 5, 2015

ott0.24 installation error :

[youngju.song@yoda]~/ott_distro_0.24% make clean
cd src; make clean
make[1]: Entering directory `/home/youngju.song/ott_distro_0.24/src'
rm -f *~ *.cmi *.cmo *.cmx *.o 
rm -f grammar_lexer.ml grammar_parser.ml                        \
              grammar_parser.mli grammar_parser.output 
rm -f version.ml
rm -rf ott ott.byt ott.opt ../bin/ott
rm -f grammar_parser.tex *.mly-y2l
rm -f *.aux *.log *.dvi *.ps *.pdf *.annot
rm -f out.thy out.v outScript.sml outTheory.uo outTheory.ui outTheory.sig outTheory.sml out.tex out.sty 
rm -f tmp_*.dot tmp.dot
rm -f tmp_*.ott
rm -f testRegr*
rm -f *Theory.* *.ui *.uo
make[1]: Leaving directory `/home/youngju.song/ott_distro_0.24/src'
rm -f *~
[youngju.song@yoda]~/ott_distro_0.24% make world
cd src; make install
make[1]: Entering directory `/home/youngju.song/ott_distro_0.24/src'
ocamllex grammar_lexer.mll
374 states, 16439 transitions, table size 68000 bytes
3397 additional bytes used for bindings
ocamlyacc -v grammar_parser.mly  
2 rules never reduced
echo 'let n="0.24"' >version.ml
echo let d=\"$(cat tmp_date.txt)\" >>version.ml
ocamldep location.ml types.ml auxl.ml merge.ml global_option.ml  grammar_lexer.ml grammar_parser.mli grammar_parser.ml version.ml grammar_pp.ml parse_ta
ble.ml glr.ml new_term_parser.ml term_parser.ml dependency.ml bounds.ml context_pp.ml grammar_typecheck.ml transform.ml substs_pp.ml subrules_pp.ml embe
d_pp.ml defns.ml ln_transform.ml coq_induct.ml system_pp.ml lexyac_pp.ml align.ml main.ml  align.mli bounds.mli coq_induct.mli defns.mli dependency.mli 
embed_pp.mli grammar_typecheck.mli merge.mli subrules_pp.mli substs_pp.mli system_pp.mli lexyac_pp.mli transform.mli term_parser.mli        > .depend  
File "grammar_typecheck.ml", line 59, characters 0-2:
Error: This comment contains an unterminated string literal
File "grammar_typecheck.ml", line 89, characters 20-26:
Error: String literal begins here
make[1]: *** [.depend] Error 2
make[1]: Leaving directory `/home/youngju.song/ott_distro_0.24/src'
make: *** [world] Error 2

@yhyoon
Copy link

yhyoon commented Apr 6, 2015

  • ott 0.24 버전을 쓰는 특별한 이유가 있는지? 최신 버전은 0.25인 것 같은데 http://www.cl.cam.ac.uk/~pes20/ott/ott_distro_0.25.tar.gz
  • 제 경우 opam으로 ocaml 패키지들 설치 -> coq8.4pl5 소스코드에서 빌드(with -usecamlp4) -> vellum-legacy에서 make libs
    여기까지 성공하고 그 다음 make에서 막혀있는 상태.

@alxest
Copy link
Author

alxest commented Apr 8, 2015

I solved with help of @jeehoonkang, @yhyoon.
Thanks a lot!

@alxest alxest closed this as completed Apr 8, 2015
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@jeehoonkang @yhyoon @alxest