I was using the newest Camlp5: Camlp5 version 6.05 (ocaml 3.12.1)
While trying to build Camlp5 5.15 I got this error:
$ make opt
set -e; for i in ocaml_stuff lib odyl main meta etc; do cd $i; make opt; cd
..; done
make[1]: Entering directory `/camlp5-5.15/ocaml_stuff'
cd 3.12.1/utils; make opt
make[2]: Entering directory `/camlp5-5.15/ocaml_stuff/3.12.1/utils'
make[2]: Nothing to be done for `opt'.
make[2]: Leaving directory `/camlp5-5.15/ocaml_stuff/3.12.1/utils'
make[1]: Leaving directory `/camlp5-5.15/ocaml_stuff'
make[1]: Entering directory `/camlp5-5.15/lib'
make[1]: Nothing to be done for `opt'.
make[1]: Leaving directory `/camlp5-5.15/lib'
make[1]: Entering directory `/camlp5-5.15/odyl'
make[1]: Nothing to be done for `opt'.
make[1]: Leaving directory `/camlp5-5.15/odyl'
make[1]: Entering directory `/camlp5-5.15/main'
make[1]: Nothing to be done for `opt'.
make[1]: Leaving directory `/camlp5-5.15/main'
make[1]: Entering directory `/camlp5-5.15/meta'
rm -f camlp5r.opt
cd ../main; make optp5 OTOP=../ocaml_stuff/3.12.1
CAMLP5OPT=../meta/camlp5r.opt CAMLP5M="-I ../meta pa_r.cmx pa_rp.cmx
pr_dump.cmx"
make[2]: Entering directory `/camlp5-5.15/main'
ocamlopt.opt ../odyl/odyl.cmxa camlp5.cmxa -I ../meta pa_r.cmx pa_rp.cmx
pr_dump.cmx ../odyl/odyl.cmx -linkall -o ../meta/camlp5r.opt
/usr/bin/flexlink: line 2: /usr/lib/flexdll/flexlink.exe: No such file or
directory
/usr/bin/flexlink: line 2: exec: /usr/lib/flexdll/flexlink.exe: cannot
execute: No such file or directory
File "caml_startup", line 1, characters 0-1:
Error: Error during linking
Makefile:27: recipe for target `../meta/camlp5r.opt' failed
make[2]: *** [../meta/camlp5r.opt] Error 2
make[2]: Leaving directory `/camlp5-5.15/main'
Makefile:23: recipe for target `camlp5r.opt' failed
make[1]: *** [camlp5r.opt] Error 2
make[1]: Leaving directory `/camlp5-5.15/meta'
Makefile:24: recipe for target `opt' failed
make: *** [opt] Error 2
I went and downloaded flexlink.exe and put it into
C:\cygwin\usr\lib\flexdll\ but I get the same error! I am new to cygwin,
so am I misunderstanding how paths work here?
On 15 March 2012 00:07, "Mark" <[email protected]> wrote:
> This is due to do with Camlp5. I'm not sure whether HOL Light properly
> supports the Camlp5 6.x versions (i.e. the latest versions). Which Camlp5
> version are you using, as a matter of interest?
> camlp5 -v
>
> I've never known HOL Light to successfully build with Camlp5 6.x, but
> according to the previous posting at least Camlp5 version 6.02.3 works for
> some people (note that 6.02.3 requires a patch, for which you must have the
> 'patch' program installed):
>
> http://sourceforge.net/mailarchive/message.php?msg_id=28674314
>
> However this does not seem to work for me! Presumably you are getting the
> same problem as me. I recommend Camlp5 version 5.15. Old versions are
> available towards the bottom of the Camlp5 page:
>
> http://cristal.inria.fr/~ddr/camlp5/
>
> This works for me with the latest HOL Light SVN download.
>
> Mark.
>
>
> on 14/3/12 5:19 PM, Adam Golding <[email protected]> wrote:
>
> > Hi, thanks for your help,
> >
> > I downloaded the new hol light via svn, and, while there are several ml
> > files that begin with 'pa_j_3.1x', they all give me this error:
> >
> > File "pa_j.ml", line 112, characters 71-73:
> > Error: This expression has type (string * MLast.ctyp) list
> > but an expression was expected of type
> > ('a * MLast.ctyp) list Ploc.vala
> > Makefile:33: recipe for target `pa_j.cmo' failed
> > make: *** [pa_j.cmo] Error 2
> >
> > On 14 March 2012 06:28, "Mark" <[email protected]> wrote:
> >
> >> You are not the first to have had trouble!
> >>
> >> The first thing is that you are trying to install HOL Light. When
> people
> >> say "HOL" they mean HOL4, which is another HOL theorem prover.
> >>
> >> The problem you get is due to there being significant changes between
> > OCaml
> >> 3.11.X and 3.12.X, and the version of HOL Light you have (presumably the
> >> snapshot from 10th Jan 2010?), does not cater for OCaml 3.12.X.
> Versions
> >> of
> >> HOL Light since the 10th Jan 2010 snapshot are only available as a
> >> Subversion snapshot.
> >>
> >> There are 3 possible solutions:
> >> 1. Download the latest HOL Light Subversion shapshot (see the HOL Light
> >> webpage). For this you need to install Subversion.
> >> 2. Tweak the version of HOL Light you have to work with OCaml 3.12.X.
> > This
> >> doesn't take long, and I can tell you how if needed.
> >> 3. Install an older version of OCaml. I've had problems installing
> OCaml
> >> 3.11.X (and OCaml 3.12.0) on 64-bit Linux, so perhaps OCaml 3.10.2 is
> the
> >> safest choice.
> >>
> >> I recommend solution 1. Another thing to remember is that you must do a
> >> "make clean" before reattempting a "make" in the same HOL Light
> directory.
> >> And another thing is that you need the right version of Camlp5 (do
> "camlp5
> >> -v" to find out).
> >>
> >> Note that there was a similar posting a few months ago:
> >> http://sourceforge.net/mailarchive/message.php?msg_id=28674314
> >>
> >> Hope this helps,
> >>
> >> Mark.
> >>
> >>
> >> on 14/3/12 9:23 AM, Adam Golding <[email protected]> wrote:
> >>
> >> > My Situation:
> >> > Windows 7 64-bit Ultimate
> >> > Cygwin (with the Cygwin version of OCaml 3.12.1)
> >> >
> >> > Since there is no pa_j_3.12.ml file I copied pa_j_3.11.ml to pa_j.ml
> >> >
> >> > I get the following error when trying to 'make' HOL:
> >> >
> >> > $ ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I
> >> +camlp5
> >> > pa_j.ml
> >> > File "pa_j.ml", line 1689, characters 37-56:
> >> > While expanding quotation "class_expr":
> >> > Parse error: ']' or [expr] expected after '[' (in [expr])
> >> > File "pa_j.ml", line 1, characters 0-1:
> >> > Error: Preprocessor error
> >> >
> >> > Not having the first clue about OCaml, I don't know how to proceed
> from
> >> > here..
> >> >
> >> > Many Thanks :-)
> >> > Adam Golding
> >> >
> >> >
> >> >
> >> > ----------------------------------------
> >> >
> >> >
> >>
> >>
> >
>
> ----------------------------------------------------------------------------
> >> > --
> >> > Virtualization & Cloud Management Using Capacity Planning
> >> > Cloud computing makes use of virtualization - but cloud computing
> >> > also focuses on allowing computing to be delivered as a service.
> >> > http://www.accelacomm.com/jaw/sfnl/114/51521223/
> >> >
> >> >
> >> > ----------------------------------------
> >> > _______________________________________________
> >> > hol-info mailing list
> >> > [email protected]
> >> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >> >
> >> >
> >> >
> >>
> >
> >
> >
>
------------------------------------------------------------------------------
This SF email is sponsosred by:
Try Windows Azure free for 90 days Click Here
http://p.sf.net/sfu/sfd2d-msazure
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
