Thanks much! Your instructions plus a "make clean" to regenerate pa_j.ml did the job.

- Cris

On Tue, Jan 3, 2012 at 7:10 AM, "Mark" <mark@proof-technologies.com> wrote:
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 <cris@perdues.com> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>