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

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

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
and dh_ocaml.

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
   hol-light instead?

Using dh_ocaml --runtime-map hol-light does generate the desired
camlp5-q9ic5 dependency.


I made the package now Architecture: any. This gives me a lintian
error 

  I: hol-light: arch-dep-package-has-big-usr-share 17934kB 100%
  N: 
  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:    
  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:    
  N:    Refer to Debian Developer's Reference section 6.7.5
  N:    (Architecture-independent data) for details.
  N:    
  N:    Severity: wishlist, Certainty: certain
  N:    
  N:    Check: huge-usr-share, Type: binary

Should I ignore this until #549679 is fixed or should I split the
package? 


I wrote:
   
   The upstream README describes howto generate an ocaml toplevel
   with hol.ml preloaded with the use of some user-level
   checkpointing tool. 

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
snapshots. 


Bye,

Hendrik