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.)
To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information