[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Re: Processing of coq_8.0pl2-1_i386.changes



On Mon, Jan 31, 2005 at 07:33:59PM +0100, Claudio Sacerdoti Coen wrote:
> > BTW: I'm also considering dropping coqtop.byte and coqide.byte from the 
> > package on native archs since they are quite big, unless someone objects 
> > to it.
> 
>  I do :-)  From the Coq manual:
> 
>  6.4.3  Declare ML Module string1 .. stringn.
>  This commands loads the Objective Caml compiled files string1 ...stringn
>  (dynamic link). It is mainly used to load tactics dynamically. The files are
>  searched into the current Objective Caml loadpath (see the command Add ML
>  Path in the section 6.5). Loading of Objective Caml files is only possible
>  under the bytecode version of coqtop (i.e. coqtop called with options -byte,
>  see chapter 12).

The solution is obviously to split the coq packages like the spamoracle or ara
packages did, in a arch: all bytecode package built only once, and a couple of
arch specific native code versions.

I am considering to make this kind of built policy for future builds.

Friendly,

Sven Luther



Reply to: