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

[Stéphane Glondu <glondu@debian.org>]

Le 19/03/2012 13:18, Hendrik Tews a écrit :
>    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.

See:


http://wiki.debian.org/Teams/OCamlTaskForce?action=AttachFile&do=get&target=jfla10-dh-ocaml.pdf

> I see hol-light as an OCaml application.

Since it uses the toplevel (which is a form of compiler), it qualifies
better as a development tool.

> 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? 

It's not an error, it's an info :-) Please override it with a useful
comment, and don't 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.

It should be possible to compile stuff so that your:

  #use "hol.ml";;

could be replaced by a much faster:

  #load "hol.cma";;

Besides, the package would also be of better quality, because it would
not be available if the compilation of hol.ml failed.


Cheers,

-- 
Stéphane