HOL Light requires Camlp5 for OCaml versions >=3.10. The problem is that
HOL Light doesn't cater for Camlp5 versions 6.X, so you must use a 5.X
version. Also note that only Camlp5 version 5.15 works for OCaml 3.12.
So, given that you have OCaml 3.12, the solution is to install Camlp5
version 5.15. Go to the Camlp5 webpage:
http://pauillac.inria.fr/~ddr/camlp5/
and scroll down towards the bottom for a link to previous versions.
Mark.
on 3/1/12 7:33 AM, 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
>
>
>
> ----------------------------------------
>
>
----------------------------------------------------------------------------
> --
> 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
>
>
>
------------------------------------------------------------------------------
Ridiculously easy VDI. With Citrix VDI-in-a-Box, you don't need a complex
infrastructure or vast IT resources to deliver seamless, secure access to
virtual desktops. With this all-in-one solution, easily deploy virtual
desktops for less than the cost of PCs and save 60% on VDI infrastructure
costs. Try it free! http://p.sf.net/sfu/Citrix-VDIinabox
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
