I am looking for suggestions on successfully running "make" to install the
current version of HOL Light.
On an Ubuntu 11.10 system, with:
$ ocaml -version
The Objective Caml toplevel, version 3.12.0
$ camlp5 -v
Camlp5 version 6.02.2 (ocaml 3.12.0)
# Running "make" I get:
$ make
if test `ocamlc -version | cut -c3` = "0" ; \
then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo"
-I +camlp4 pa_j.ml; \
else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo
q_MLast.cmo" -I +camlp5 pa_j.ml; \
fi
File "pa_j.ml", line 112, characters 72-74:
Error: This expression has type (string * MLast.ctyp) list
but an expression was expected of type
('a * MLast.ctyp) list Ploc.vala
make: *** [pa_j.cmo] Error 2
This was done in the root directory after syncing this afternoon to the SVN
directory at Google code.
The README suggests that the default location of the camlp5 library in in
/usr/local. I have done:
$ export CAMLP5LIB=/usr/lib/ocaml/camlp5
# camlp5 library:
$ echo $CAMLP5LIB
/usr/lib/ocaml/camlp5
cris@cris-netbook:~/src/hol-light-read-only$ ls !$
ls $CAMLP5LIB
camlp5.a gramext.mli pa_extend.o pa_macro.cmx
pa_pragma.o ploc.cmi pr_null.cmo prtools.cmi
camlp5.cma gramlib.a pa_extfold.cmo pa_macro.o pa_r.cmo
ploc.cmx pr_null.cmx prtools.mli
camlp5.cmxa gramlib.cma pa_extfold.cmx pa_mkast.cmo pa_r.cmx
ploc.mli pr_null.o q_ast.cmo
camlp5o.cma gramlib.cmxa pa_extfold.o pa_mkast.cmx
pa_reloc.cmo pprintf.cmi pr_o.cmo q_ast.cmx
camlp5r.cma grammar.cmi pa_extfun.cmo pa_mkast.o
pa_reloc.cmx pprintf.cmx pr_o.cmx q_ast.o
camlp5sch.cma grammar.cmx pa_extfun.cmx pa_mktest.cmo
pa_reloc.o pprintf.mli pr_o.o q_MLast.cmo
camlp5_top.cma grammar.mli pa_extfun.o pa_mktest.cmx pa_r.o
pr_depend.cmo pr_op.cmo q_MLast.cmx
diff.cmi lib.sml pa_extprint.cmo pa_mktest.o pa_rp.cmo
pr_depend.cmx pr_op.cmx q_MLast.o
diff.cmx META pa_extprint.cmx pa_o.cmo pa_rp.cmx
pr_depend.o pr_op.o q_phony.cmo
diff.mli mLast.cmi pa_extprint.o pa_o.cmx pa_rp.o
pr_dump.cmo pr_r.cmo q_phony.cmx
eprinter.cmi mLast.mli pa_fstream.cmo pa_o_fast.cmx
pa_scheme.cmo pr_dump.cmx pr_r.cmx q_phony.o
eprinter.cmx ocpp.cmo pa_fstream.cmx pa_o_fast.o
pa_scheme.cmx pr_dump.o pr_r.o quotation.cmi
eprinter.mli odyl.a pa_fstream.o pa_o.o
pa_scheme.o pretty.cmi pr_ro.cmo quotation.mli
extfold.cmi odyl.cma pa_lefteval.cmo pa_oop.cmo
pa_sml.cmo pretty.cmx pr_ro.cmx reloc.cmi
extfold.cmx odyl.cmo pa_lefteval.cmx pa_oop.cmx
pa_sml.cmx pretty.mli pr_ro.o reloc.mli
extfold.mli odyl.cmx pa_lefteval.o pa_oop.o pa_sml.o
pr_extend.cmo pr_rp.cmo stdpp.cmi
extfun.cmi odyl.cmxa pa_lexer.cmo pa_op.cmo pcaml.cmi
pr_extend.cmx pr_rp.cmx stdpp.cmx
extfun.cmx odyl.o pa_lexer.cmx pa_op.cmx pcaml.mli
pr_extend.o pr_rp.o stdpp.mli
extfun.mli pa_extend.cmi pa_lexer.o pa_op.o
plexer.cmi pr_extfun.cmo pr_scheme.cmo token.cmi
fstream.cmi pa_extend.cmo pa_lisp.cmo pa_pprintf.cmo
plexer.cmx pr_extfun.cmx pr_scheme.cmx token.cmx
fstream.cmx pa_extend.cmx pa_lisp.cmx pa_pprintf.cmx
plexer.mli pr_extfun.o pr_scheme.o token.mli
fstream.mli pa_extend_m.cmo pa_lisp.o pa_pprintf.o
plexing.cmi pr_extprint.cmo pr_schemep.cmo versdep.cmi
gramext.cmi pa_extend_m.cmx pa_macro.cmi pa_pragma.cmo
plexing.cmx pr_extprint.cmx pr_schemep.cmx versdep.cmx
gramext.cmx pa_extend_m.o pa_macro.cmo pa_pragma.cmx
plexing.mli pr_extprint.o pr_schemep.o
Thanks much for any help.
Regards,
-Cris
------------------------------------------------------------------------------
Write once. Port to many.
Get the SDK and tools to simplify cross-platform app development. Create
new or port existing apps to sell to consumers worldwide. Explore the
Intel AppUpSM program developer opportunity. appdeveloper.intel.com/join
http://p.sf.net/sfu/intel-appdev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
