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
--
To UNSUBSCRIBE, email to debian-wnpp-requ...@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
Archive: http://lists.debian.org/20323.6066.37102.182...@blau.inf.tu-dresden.de
