Thanks much! Your instructions plus a "make clean" to regenerate
pa_j.mldid the job.
- Cris
On Tue, Jan 3, 2012 at 7:10 AM, "Mark" <[email protected]> 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 <[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
