John, here's my bug report for trying to install the latest ocaml &
camlp5.   `make' failed in hol_light (error message at the end).

I'm an 64 bit Dell Linux box running Scientific Linux:

(poisson)ocaml-3.12.1> uname -a
Linux poisson.math.northwestern.edu 2.6.32-220.4.1.el6.x86_64 #1 SMP
Mon Jan 23 17:20:44 CST 2012 x86_64 x86_64 x86_64 GNU/Linux

I untarred ocaml-3.12.1.tar.gz camlp5-6.05.tgz and

(poisson)ocaml-3.12.1> ./configure -prefix /rhome/2/richter/HOL-Light
(poisson)ocaml-3.12.1> make world > log.world 2>&1 &
(poisson)ocaml-3.12.1> make bootstrap > log.bootstrap 2>&1 
(poisson)ocaml-3.12.1> make world > log.world 2>&1 &
(poisson)ocaml-3.12.1> make bootstrap > log.bootstrap 2>&1 
(poisson)ocaml-3.12.1> make opt > log.opt 2>&1 
You have mail in /var/spool/mail/richter
(poisson)ocaml-3.12.1> make opt.opt
make install

Seemed to install fine.  

(poisson)camlp5-6.05> ./configure -prefix /rhome/2/richter/HOL-Light

Resulting configuration file (config/Makefile.cnf):

MODE=S
EXE=
OPT=.opt
EXT_OBJ=.o
EXT_LIB=.a
OVERSION=3.12.1
VERSION=6.05
VERSDIR=
OTOP=$(TOP)/ocaml_stuff/3.12.1
OCAMLC_W_Y="-w y"
WARNERR="-warn-error A"
NO_PR_DIR=--no-print-directory
OLIBDIR=/rhome/2/richter/HOL-Light/lib/ocaml
PREFIX=/rhome/2/richter/HOL-Light
BINDIR=$(PREFIX)/bin
LIBDIR=$(PREFIX)/lib/ocaml
MANDIR=$(PREFIX)/man
OCAMLN=ocaml
CAMLP5N=camlp5

=== strict mode ===

Strict is the default; I didn't know that.  We see ocaml is installed:

(poisson)camlp5-6.05> which ocaml
/rhome/2/richter/HOL-Light/bin/ocaml

(poisson)camlp5-6.05> make world.opt
seemed to work fine!  Now install:

(poisson)camlp5-6.05> make install

And it seems to have worked!

(poisson)camlp5-6.05> ls $HOME/HOL-Light/bin
camlp4*         camlp4prof*    camlp5sch*          ocamlcp*       ocamlobjinfo*
camlp4boot*     camlp4r*       mkcamlp4*           ocamldebug*    ocamlopt*
camlp4o*        camlp4rf*      mkcamlp5*           ocamldep*      ocamlopt.opt*
camlp4of*       camlp4rf.opt*  mkcamlp5.opt*       ocamldep.opt*  ocamlprof*
camlp4of.opt*   camlp4r.opt*   ocaml*              ocamldoc*      ocamlrun*
camlp4oof*      camlp5*        ocamlbuild*         ocamldoc.opt*  ocamlyacc*
camlp4oof.opt*  camlp5o*       ocamlbuild.byte*    ocamllex*      ocpp5*
camlp4o.opt*    camlp5o.opt*   ocamlbuild.native*  ocamllex.opt*
camlp4orf*      camlp5r*       ocamlc*             ocamlmklib*
camlp4orf.opt*  camlp5r.opt*   ocamlc.opt*         ocamlmktop*

Now I'll build the latest version of HOL Light:


(poisson)~> svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light
[...]
Checked out revision 135.

(poisson)hol_light> export 
LD_LIBRARY_PATH=$HOME/HOL-Light/lib:/rhome/richter/Gambit/current/lib
(poisson)hol_light> make

(poisson)hol_light> make
\
        if test `ocamlc -version | cut -c3` = "0" ; \
        then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \
        else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut 
-c1-6` = "6.02.1" ; \
             then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
             else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | 
cut -c1-6` = "6.02.2" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | 
cut -c1-6` = "6.02.3" ; \
                  then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
                  else cp pa_j_3.1x_`camlp5 -v 2>&1 | cut -f3 -d' ' | cut 
-c1`.xx.ml pa_j.ml; \
                  fi \
             fi \
        fi
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 195, characters 6-21:
Error: The constructor PaLab expects 2 argument(s),
       but is applied here to 3 argument(s)
make: *** [pa_j.cmo] Error 2


I have no idea what that means.  Lines 195--7 of pa_j.ml are 

    | PaLab loc x1 x2 ->
        let loc = floc loc in
        PaLab loc (self x1) (vala_map (option_map self) x2)

I'll go try this at home on an old 32 bit machine.

-- 
Best,
Bill 

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to