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" <[email protected]> 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 <[email protected]> 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 > > <[email protected]>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 > >> [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 > >> > >> > > > > > > > > ---------------------------------------- > > > > > ---------------------------------------------------------------------------- > > -- > > 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 > > > > > > ------------------------------------------------------------------------------ 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
