On Tue, Nov 30, 2004 at 10:12:38AM +0100, Claudio Sacerdoti Coen wrote:
> Right, Coq does a lot of marshalling/umarshalling that also involves
> camlp4 data structures. And moreover there is coqide that uses threads
> and lablgtk2. The perfect mix of problems...
Well, if coqide is binary only and does not perform dynamic loading of
bytecode objects there should be no problem with it. Regarding coq
marshalling/unmarshalling, it should be affected only if the in memory
representation of camlp4 types has changed in ocaml 3.08.2, a simple new
function in a .mli doesn't imply it.
But since theory is doomed to be slanted by practice: could you, or
someone else using Coq, please give it a try after 3.08.2 update? :)
Cheers.
--
Stefano Zacchiroli -*- Computer Science PhD student @ Uny Bologna, Italy
zack@{cs.unibo.it,debian.org,bononia.it} -%- http://www.bononia.it/zack/
If there's any real truth it's that the entire multidimensional infinity
of the Universe is almost certainly being run by a bunch of maniacs. -!-
Attachment:
signature.asc
Description: Digital signature