The Coq mailing list

["Nickolay V. Shmyrev" <nshmyrev AT yandex.ru>]

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?