This page is to help new users to get HOL-Light installed and running

HOL-Light will run on almost any operation system (Windows, Linux, OSX,...). The download page is HOL-Light. Detailed installation instructions can be found in Harrison's tutorial on page 5. Cygwin is not needed to run HOL-Light on Windows.

HOL Light on Windows

This section describes how to make a simple installation on Windows.

• Your computer needs to be able to use files with extensions .tar and .tgz. If your computer does not recognize these file extensions, you should download and install PowerArchiver on your computer (which has a free trial period).

• You will need to install Objective CAML 3.09.3 on your computer. Download it here. On that page, click on the link MinGW-based native Win32 port (3.09.3).. Do not install the latest version 3.10 or later. You want an old version of Objective CAML (3.09.3).

• HOL-Light download here. It is recommended that you choose a recent version (at least 2009). (One reason to use this version is that it has a "search" command that allows you to search for the name of theorems.) The Flyspeck project has now switched from version 2.20 to the version from February 2008, which is available from the download page. When you unpack hol_light, you should have a directory called hol_light, which you can put anywhere. For instance, you can leave it on your desktop.

• You can open a new CMD prompt by choosing START, RUN, cmd, OK. Change the directory with the DOS command CD to make hol_light the current directory.

• For HOL-Light to run for the first time, you also need to create a files called pa_j.cmo and pa_j.cmi in your hol_light directory. If you know somebody else who has created these files using the same versions of Objective CAML and HOL-Light, you can copy their files. Otherwise, you need to create them yourself as follows. Rename the file pa_j_3.09.ml to pa_j.ml. At the command prompt in the hol_light directory type: ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I +camlp4 pa_j.ml This should create the files pa_j.cmo and pa_j.cmi.

• To start HOL Light. The quickest way to get started is with the command window (cmd). Eventually, you will want to start HOL Light in a way that makes a session easier to edit.
• To start HOL-Light at the cmd prompt in the hol_light directory, type ocaml and hit return. Objective CAML should start. At the Caml prompt, type #use "hol.ml;; and hit return. HOL-Light should start up. On most computers it takes a few minutes to start up.
• To start HOL-Light in the Objective CAML graphical user interface. (This section needs to be written.)
• To start HOL-Light inside Emacs. First install Emacs on Windows, as described below. Then open emacs and type "alt-x shell" This will open the command shell inside emacs. You can then follow the instructions for starting HOL-Light at the cmd prompt in the hol_light directory.

Using the Flyspeck Google Code with Windows

• If you wish to make contributions to the Flyspeck project, you will need to contact Tom Hales to be added as a project member. For this you need a gmail account. Your name will appear as a project member on the Flyspeck home page. You do not need to be a project member if you do not contribute to the Flyspeck project.

Tortoise SVN and Google Code

• To use the source files, download TortoiseSVN for Windows. You can use it to keep your files in sync with the HOL-Light code at the Flyspeck Project page. A good tutorial that tells how to download and upload files to the flyspeck website is at TortoseSVN for Google Code These instructions tell you how to obtain your password. (If you don't use your password when you download your files, you will not be able to upload them again.) In these instructions, whenever it says to type

  <project>

  , type flyspeck instead. You want to follow steps 1.0, 3.0, and 4.0 that tell you how to check out an existing project and then how to upload the files that you add to the project. After you finish step 3.0, put the file you want to upload in the same directory with all the text_formalization/ files. Highlight the file in the directory and right click on "TortoiseSVN >> Add" to add the file to the project. Then right click on "SVN Commit" to upload it.

Here are the instructions from Nguyen Duc Phuong:

• Step 1: download the latest version of Tortoisesvn, now is version 1.5.3 then install it.

• Step 2: right-mouse click on the desktop and choose SVNcheckout, then :

URL of repository: "link of the file that your group is now working on" for example, my group is workoing over: https://flyspeck.googlecode.com/svn/trunk/text_formalization/collect_geom.ml Checkout directory: you choose where the file ( whose link is above) will be put there. For example: C:\Documents and Settings\ndphuong\Desktop\text_formalization\

• Step 3: whenever the file had been downloaded to your computer, you can use msword to edit it as you want. And then right-mouse click on that file, choose SVNcommit. Your work will be uploaded and you can check it by revisiting Flyspeck google homepage.

From now on, after you had finished installed tortoisesvn, everytime you want to upload files let do from step 2 and so on. Enjoy your work by seeing them (next to your name ^.^) appear in Flyspeck googlepage !

WARNING: If you checkout using http://..., you will not be able to check it back in. (It will ask for your password, but not accept your password.) You must first checkout using https://.... if you plan to check back in.

Using Emacs on Windows

Eventually, you will want to edit HOL-Light sessions with a powerful text editor. To install the emacs editor, follow steps 1,2,3,4,8 (or all steps for a full installation) of how to install emacs.

After installing emacs, you should install the major mode hol-light-mode. This can be found in the flyspeck emacs directory.

Checkpointing

Since ocaml provides no method for storing the current state of the toplevel, it becomes useful to have an external utility that can start/stop a ocaml process that has hol/flyspeck already loaded into memory.

One way to achieve this, is to build Berkeley Lab Checkpoint/Restart. This is only applicable to certain versions of linux. Even if you do not run Linux, you can always use VirtualBox to host a copy of Linux on your current OS.

BLCR only works on Linux kernel versions <= 2.6.30. One distribution of Linux which has been tested with this setup is Ubuntu Hardy Desktop.

I found that once BLCR is configured, one should run

cr_run ocampl -I hol_light -I text_formalization

where ocampl is as in flyspeck/text_formalization/strictbuild.hl, hol_light is the path to the directory containing the source of hol_light, and text_formalization is the path to the text_formalization in the flyspeck directory. This will open ocaml. You should then issue #use "hol.ml";; and #use "strictbuild.ml";; or whatever you do not want to have to sit through every time you want to start working. After waiting for ocaml to finish, you can then run ps -A to find the PID for ocaml. Then run

cr_checkpoint -f <filename.cr> --term <ocaml PID>,

where filename.cr is what you want to call the saved process. Then whenever you want to restart just run

cr_restart --no-restore-pid -S 2 <filename.cr>.

It would probably be convenient to make a bash script called hol_light on your PATH so that running from emacs in hol-light-mode is simplified.

The advantage of BLCR is that multiple instances of the same image can be active at once. Also the images can be migrated to other computers with the same kernel. I have not personally tested the claim about migration, but this is what the BLCR claims to be able to do.

Making a version of Objective CAML with "num" preloaded

In Windows, the library nums.cma is generally preloaded. In unix/linux/Mac OS X, a new top level can be created (called ocamlnum with "num" preloaded. Just execute ocamlmktop -o ocamlnum nums.cma from the directory that contains the ocaml executable. Type which ocaml to determine the directory.