Emacs + Coq taking 100% RAM and CPU…
If this continues as-is, I will need a cluster just to develop >:-(
The issue seems to be that, in addition to Emacs filling the RAM, #Coq needs a lot of memory each time it loads a module. As a consequence, if you try to make your code more modular… you will need a ridiculous additionnal amount of RAM. This is just crazy! :'(
While googling, I’ve found the “Optimize Proof, Optimize Heap” commands.
https://github.com/coq/coq/pull/6497
https://lists.gforge.inria.fr/pipermail/coq-commits/2014-November/013694.html
I will try them ☺
https://coq.inria.fr/distrib/current/refman/proof-engine/proof-handling.html?highlight=optimize#coq:cmd.optimize-heap
By the way, I like the new style of Coq’s online documentation ☺
What I really don't understand is that this only happens in interactive mode! When compiling the files, it takes significantly less memory! What is happenning?! :-(
@MartinShadok Probably totally unrelated but Merlin sometimes eats up all my memory when I edit OCaml code. Have you tried closing Emacs, maybe killing some processes and re-opening the files?
@otini @MartinShadok And it's the same with Idris mode :/
@MartinShadok @typochon @otini I don't know what is the state of ProofGeneral maintenance and development.
@MartinShadok I wait for a better coqdoc now.
And I really wish we will one day be able to have truly private functions in Coq’s module, that is not exported (and not in coqdoc output).
@lthms To have a real Coq module system… I agree, that would be very helpful.
I've heard that Coq's module system is criticated a lot. If two required files require a common third file, Coq doesn't load this third common file twice, right? :-/