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 -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]
