Why3 uses too much memory
This is a meta-issue to summarize all the discussions into a single place.
Things to do:
Do not precompute
Decl.d_sysms, as they consume about 15% memory.
split_vcso that it introduces premises by itself instead of relying on
introduce_premises. The latter has too little information to share common declarations between subtasks. This should make the memory consumption linear rather than quadratic in the number of proof obligations.
Decl.known_add_decl, as its
Mid.unioncall seems responsible for about 25% memory consumption.
Termcode.task_v3, as its
Mid.addcall seems responsible for about 25% memory consumption.
master branch supports memory profiling, when using a suitable compiler, e.g., the one from the Opam switch
4.07.1+statistical-memprof. First, configure Why3 with
--enable-statmemprof and build it. Then, execute
bin/why3ide -L examples/multiprecision examples/multiprecision/toom. Once the interface is loaded, execute
sturgeon-connect in Emacs to see the memory consumption. (See Statmemprof's documentation for details about Sturgeon.)