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. -
Change split_vc
so that it introduces premises by itself instead of relying onintroduce_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. -
Investigate Decl.known_add_decl
, as itsMid.union
call seems responsible for about 25% memory consumption. -
Investigate Termcode.task_v3
, as itsMid.add
call seems responsible for about 25% memory consumption.
Remark: The 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.)