Great! About checkpointing, as far as I know, this works only under Linux :(
Cheers, V. On Sat, Mar 17, 2012 at 4:30 AM, Adam Golding <[email protected]> wrote: > 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 -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ ------------------------------------------------------------------------------ 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
