Downloading/Developing HOL4 Sources with Git (Anonymously)

The first thing you need to do is check out a copy of the HOL repository from Github. This is easy! There’s just one step:

   git clone git://github.com/HOL-Theorem-Prover/HOL.git

Alternatively, if you’re happy to work with Github yourself, you can always create a fork of our code there. This is the best way to then be in a position to make your own contributions to HOL.

Cloning will download a complete copy of all the current sources and install them in a directory called HOL. This is not the same thing as the source tree we distribute, but differs only slightly (it has more stuff). You will now have a copy of the sources and should be able to build hol in the normal way:

   sml-system < tools/smart-configure.sml
   bin/build

(where sml-system is one of mosml or poly).

The really nice thing about this copy of the sources is that if there is a check-in changing the sources, you can automatically patch your copy of the sources to reflect this by typing git pull in the HOL directory. Also, the git status command will tell you if you have modified any of the files in the distribution.

You can tell if there’s been a check-in to the main github repository by subscribing to the hol-checkins mailing list. Subscribe to this mailing list here. You can check the archives for the list (and see what you might be letting yourself in for) by following the link on the above page.

Developing HOL

As git is a distributed version control system, it is easy for you to make your own local commits to your copy of the repository. If you’d additionally like to have those commits incorporated into the official repository, you need to issue what is known as a “pull request”. You will first need to push your version of the repository onto Github (which you may already have set up if you forked our code there). Then you follow the process described here (Github documentation).


Time-stamp: "Sunday, 16 November 2014; 22:46 UTC (Michael Norrish)"