Re: Processing of coq_8.0pl2-1_i386.changes
Hum... Right then :)
FWIW here's an example of why I did want to build the libraries on all
bin/coqtop.opt -boot -translate -strict-implicit -nois -compile
make: *** [theories7/Init/Notations.vo] Segmentation fault
make: Leaving directory `/build/buildd/coq-8.0pl2'
WARNING: NATIVE CODE COMPILATION FAILED
Trying to build coq in bytecode instead
(on IA64, it goes on well in bytecode).
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
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).