The Coq mailing list

[Julien Narboux <Julien.Narboux AT inria.fr>]

Hello,

Ocaml does not allow dynamic loading of modules (in native code).
But Fabrice Le Fessant has implemented "Asmdynlink: a Virtual Machine 
for Ocaml bytecode written in Ocaml, to dynlink bytecode modules in 
native code programs (distributed in the CDK)".

I don't know if it is still maintained.

Regards

Julien Narboux

Nickolay V. Shmyrev a écrit :
> Hello.
>
> While working with CoRN repository I've noticed that Coq very
> extensively use memory. It requires around 40 Mb for rather simple
> proofs and when advanced tactics like "rational" are used, it may take
> more then 200 Mb and even fail to compile correct proof. Why is it so
> big and is there any way to optimize memory usage?
>
> In CoRN, there is also ml-based implementation of rational tactic, it
> much more quick, but it requires top level building. Is it planned to
> implement the dynamic loading of ml modules? If so, how dynamic loading
> can be implemented?
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club