Re: [Hol-info] Cannot Make HOL on OCaml 3.12 in Cygwin

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Ok, this last problem was a simple one--I had to add C:\cygwin\bin to
PATH and C:\cygwin\lib\ocaml to OCAMLLIB--that this was not done
automatically strikes me as an error on the part of the cygwin
installer.

So, this produced success:

1. complete uninstall of cygwin, ocaml, etc.
2. svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light
3. download and extract extract camlp5-6.02.0, go to its dir
4. add C:\cygwin\lib\ocaml to path
5. add C:\cygwin\bin to PATH
6. add C:\cygwin\lib\ocaml to OCAMLLIB
7. follow the instructions in the campl5 "INSTALL" files
8. hol_light make
9. set HOLLIGHT_DIR = C:\cygwin\hol_light
10. campl
11. #use hol.ml;;

The examples in harrison's tutorial appear to be working now--however,
I have no idea how to attempt the 'standalone' installation described
further into the hol light "README" file--what 'checkpointing' tool is
appropriate for cygwin?  A previous poster said that standalone mode
would not work in my case--is that because there is no checkpointing
tool for cygwin?

On 16 March 2012 22:37, "Mark" <ma...@pr...> wrote:
>
> Hi Adam,
>
> This must be so frustrating for you.  You have my sympathies.  I'm also
> finding problems getting any HOL Light working with any Camlp5 6.X (I am
> using OCaml 3.12.1).  I'm guessing the problems are a combination of a
> flakey Camlp5 6.X - apparently it changed quite a bit from 5.X - and poor
> support in HOL Light for Camlp5.  I'm going to try to look into this later
> today if I find a chance.  I can probably tweak a couple of files that come
> with HOL Light and find a suitable version of Camlp5 6.X and get this
> working for you.  Although I am using Linux, which may also be a crucial
> difference.
>
> In the mean time, please try again Camlp5 5.15.  This works for me in Linux
> with OCaml 3.12.1 and all versions of HOL Light from the 2010-01-10 snapshot
> onwards.  When installing Camlp5, I do:
>   ./configure --transitional
>   make world.opt
>   make install
>
> One tip if you are experimenting with various versions of Camlp5 for the
> same version of OCaml is to do the above three steps for each version,
> without doing a subsequent "make clean" for any of them.  Then, to try a
> given Camlp5, simply do "make install" for the version you want to try.  The
> install command just puts the Camlp5 executables in the bin directory for
> the version of OCaml that you are using, overwriting any others from other
> versions of Camlp5, and only takes a couple of seconds (as opposed to a
> couple of minutes each time you do "make world.opt").
>
> And please confirm the precise version of OCaml (e.g. 3.12.1).
>
> Mark.
>
> on 16/3/12 8:37 PM, Adam Golding <ada...@ad...> wrote:
>
> > I now have this problem:
> >
> > 1. uninstall, delete, and reinstall cygwin
> > 2. svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light
> > 3. extract camlp5-6.02.0
> > 4. ./configure --strict
> >
> > user@X220 /camlp5-6.02.0
> >
> > $ ./configure --strict
> >
> >>> Fatal error: cannot open pervasives.cmi
> >
> > Fatal error: exception Misc.Fatal_error
> >
> >>> Fatal error: cannot open pervasives.cmi
> >
> > Fatal error: exception Misc.Fatal_error
> >
> > Resulting configuration file (config/Makefile.cnf):
> >
> > MODE=S
> >
> > EXE=
> >
> > OPT=.opt
> >
> > EXT_OBJ=.o
> >
> > EXT_LIB=.a
> >
> > OVERSION=3.12.1
> >
> > VERSION=6.02.0
> >
> > OTOP=$(TOP)/ocaml_stuff/3.12.1
> >
> > OCAMLC_W_Y="-w y"
> >
> > WARNERR="-warn-error A"
> >
> > NO_PR_DIR=--no-print-directory
> >
> > OLIBDIR=C:\cygwin\opt\lib\ocaml
> >
> > BINDIR=/usr/bin
> >
> > LIBDIR=C:\cygwin\opt\lib\ocaml
> >
> > MANDIR=/usr/man
> >
> > === strict mode ===
> >
> > 1. add C:\cygwin\lib\ocaml to path
> >
> > then I get the same error again..
> >
> > On 15 March 2012 03:51, Vincent Aravantinos
> > <vin...@gm...>wrote:
> >
> >> Adding my own 2 cents...
> >>
> >> HOL light should work fine with Ocaml 3.12 (at least I'm using it every
> >> day with it), but the version of camlp5 is quite important since camlp5
> is
> >> under permanent development and undergoes quites many changes.
> >>
> >> So, to sum up, the following worked for me recently (not tested under
> >> Cygwin though): ocaml 3.12.x + camlp5 6.02.0 (be very careful: not 6.02.1
> >> or 6.01.99!)
> >> You can access older versions of camlp5 at
> >> http://pauillac.inria.fr/~ddr/camlp5/distrib/src/?C=M;O=A.
> >>
> >> About your flexlink problem, I would not be surprised that it comes from
> >> your successive installations of ocaml 3.12 and ocaml 3.11.
> >> I would suggest to just remove everything and start over.
> >>
> >> Cheers,
> >> V.
> >>
> >> --
> >> Vincent Aravantinos
> >> PostDoctoral fellow, Concordia University, Hardware Verification Group
> >> http://users.encs.concordia.ca/~vincent
> >>
> >> Le 14 mars 12 à 02:58, Adam Golding a écrit :
> >>
> >> 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
> >> hol...@li...
> >> 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
> >> hol...@li...
> >> 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
> > hol...@li...
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
> >
> >