GitLab

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 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.
• Investigate Decl.known_add_decl, as its Mid.union call seems responsible for about 25% memory consumption.
• Investigate Termcode.task_v3, as its Mid.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.)