Hum... Right then :)
FWIW here's an example of why I did want to build the libraries on all archs [1]:
bin/coqtop.opt -boot -translate -strict-implicit -nois -compile theories7/Init/Notations
make[1]: *** [theories7/Init/Notations.vo] Segmentation fault
make[1]: 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).
Cheers,
Samuel.
[1] http://buildd.debian.org/fetch.php?&pkg=coq&ver=8.0pl2-1&arch=ia64&stamp=1107195335&file=log&as=raw
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).
Cheers, C.S.C.
-- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]
