[isabelle-dev] [isabelle] Status of HOL/Import

[Cezary Kaliszyk]

On Wed, Jul 13, 2011 at 4:51 PM, Alexander Krauss <krauss at in.tum.de> wrote:
> On 07/12/2011 11:15 PM, Florian Haftmann wrote:
> I just tried to redo this to see how it works
> $ svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light
> $ cd hol_light/Proofrecording/hol_light
> $ make
> and it failed with
> [...]

The issue is with versions of OCaml. The HOL Light distribution
includes a number of versions of the parser (files pa_j_XXX.ml)
that are supposed to work with particular versions of OCaml.
I am using an old version of OCaml for HOL Light (3.10.2)
however the distribution includes some pa_j_ files for versions 3.11.XXX.
Also make sure that camlp5 has the same version as ocaml; as
this is not the case for example on macbroys.

One more suggestions, try to run 'make' in the top directory of
hol light first; after this works you can copy pa_j.ml and pa_j.cm* to
ProofRecodring/hollight.

> Also, what is the HOL Light release policy? Is everybody really just using
> the svn head?

Last named release (2.20) was in 2005, since then John Harrison sometimes
packs versions considered "more stable". Otherwise it is the SVN.

Cezary