On Wed, Jul 13, 2011 at 4:51 PM, Alexander Krauss <kra...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
