Re: Bug#663754: ITP: hol-light -- HOL Light theorem prover
Stéphane Glondu writes:
camlp5 is a development package, not a runtime one. From your
description, hol-light would also be a development package.
I am sorry, but I don't understand the distinction between
runtime and development packages and its importance for packaging
I see hol-light as an OCaml application.
Did you try
to run dh_ocaml with --runtime-map (the same way as camlp5 does) in
Using dh_ocaml --runtime-map hol-light does generate the desired
I made the package now Architecture: any. This gives me a lintian
I: hol-light: arch-dep-package-has-big-usr-share 17934kB 100%
N: The package has a significant amount of architecture-independent data
N: (over 4MB, or over 2MB and more than 50% of the package) in /usr/share
N: but is an architecture-dependent package. This is wasteful of mirror
N: space and bandwidth since it means distributing multiple copies of this
N: data, one for each architecture.
N: If the data in /usr/share is not architecture-independent, this is a
N: Policy violation that should be fixed by moving the data elsewhere
N: (usually /usr/lib).
N: Refer to Debian Developer's Reference section 6.7.5
N: (Architecture-independent data) for details.
N: Severity: wishlist, Certainty: certain
N: Check: huge-usr-share, Type: binary
Should I ignore this until #549679 is fixed or should I split the
The upstream README describes howto generate an ocaml toplevel
with hol.ml preloaded with the use of some user-level
I don't think we should package snapshots with hol.ml preloaded.
The problem is that such snapshot images contain all needed
shared libraries and would have to get updated whenever there is
a security update of one of those libraries.
The README.Debian explains now how to use dmtcp to create