This page is to help new users to get HOL-Light installed and runningHOL-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 WindowsThis 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).
- 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 WindowsEventually, 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. This section needs to be filled in. CheckpointingThis section needs to be filled in. Making a version of Objective CAML with "num" preloadedIn 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.
|
Sign in to add a comment
