I have been able to replicate John Rugis positive result in building and
running HOL Light under Ubuntu 11.10 using ocaml 3.12 and camlp5 version 6
(6.02.3).
In the camlp5 directory I have done:
$ make clearn
$ configure --strict
$ make world.opt
$ sudo make install
Note that the default install directories are /usr/bin and /usr/lib rather
than /usr/local/...
$ camlp5 -v
Camlp5 version 6.02.3 (ocaml 3.12.0)
In the hol-light directory I did:
$ make clean
$ make
Running HOL light succeeds and at the end of initialization prints:
Camlp5 parsing version 6.02.3
Thanks Mark and both Johns for your communications on this.
-Cris
On Mon, Jan 2, 2012 at 6:25 PM, Cris Perdue <[email protected]> wrote:
> 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
>
>
------------------------------------------------------------------------------
RSA(R) Conference 2012
Mar 27 - Feb 2
Save $400 by Jan. 27
Register now!
http://p.sf.net/sfu/rsa-sfdev2dev2
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
