Re: Bug#663754: ITP: hol-light -- HOL Light theorem prover

[Hendrik Tews <tews@os.inf.tu-dresden.de>]

Hi,

a first version of the hol-light package is available at
git://git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git 

Comments are welcome!

The current package has the following issues:

- the precise upstream license is not clear yet, I've asked
  upstream about it, see the messages at Bug#663754

- the dependencies of the binary package on camlp5 are not right,
  see below

I believe we need to change the camlp5 package to provide a
virtual package with its ABI version, similar to
ocaml-base-nox-3.12.1, see below.



Notes on the package:

Installation of HOL Light means to compile a small camlp5 syntax
extension and copy the sources somewhere. When you want to run
HOL Light, you start an ocaml toplevel and do 
``#load "..../hol-light/hol.ml";;'' This loads the logical core
and the basic results (which takes about 2 minutes).

The package installs the (almost) complete upstream sources in
/usr/share/hol-light. The syntax extension is compiled as
pa_j.cmo and also installed there. There is a script
/usr/bin/hol-light for starting the toplevel and loading hol.ml.

I believe the compiled syntax extension will only work with the
camlp5 version it was compiled. Therefore I would like to have a
dependency 

 camlp5-${F:Camlp5ABI},

with

CAMLP5_ABI ?= $(shell /usr/bin/camlp5 -v 2>&1 | { read a b c d && echo $$c; })

and 

	dh_gencontrol -- -VF:OCamlABI="$(OCAML_ABI)" \
		-VF:Camlp5ABI="$(CAMLP5_ABI)"

This does of course not work, because there is no package
camlp5-6.04. Can we change the camlp5 package to provide
camlp5-${F:Camlp5ABI} ?


The upstream README describes howto generate an ocaml toplevel
with hol.ml preloaded with the use of some user-level
checkpointing tool. This should work on i386 and amd64 and would
certainly be useful. I leave this point for the next version of
the package.

Some people are working on supporting hol-light in Proof General.
This is however not complete yet. Hopefully, I can incorporate
hol-light support in Proof General with the next Proof General
release. 

Bye,

Hendrik