[isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 28/10/17 22:26, Makarius wrote:
>
> I still have some ideas for "isabelle build" in the pipeline (for
> several years) to skip building intermediate heaps in the first place.
> Then AFP (without the "slow" sessions) could shrink to 50% .. 20% build
> time.
> 
> Until that emerges, AFP contributors may want to double-check, which
> auxiliary heaps ("Base", "Lib", "Pre") are really needed and beneficial
> for overall build times.

That now came out as options for "isabelle jedit", instead of more
"isabelle build" technology (and complexity).


Here is a summary of the present situation:

  * Poly/ML 5.7.1 (testing version) is quite fast in loading heaps, but
there are also file-system accesses and time to build heaps in the first
place (which also means full sharing of live data: at the order of 30s).

  * It does not make sense to refer to a parent session and then use
only a few small theories that require < 10s. Above 30s a parent that is
itself not too bulky usually helps.

  * Building a heap with many ancestors is more expensive than a rather
flat hierarchy. There is a small overhead in the Poly/ML runtime system
for managing the dynamic hierarchy, but more relevant are redundant
imports: a big stack of heaps usually contains many theories that are
not needed in the final application.

  * http://isabelle.in.tum.de/devel/build_status/AFP/index.html shows
some of the data that accumulates in one big Isabelle test database.
There is more than than shown here, e.g. individual theory timings
(which are meaningful for these builds with threads=1).

In the exploration, I've occasionally emitted handwritten SQL statements
to the PostgreSQL engine via the web interface of phppgadmin. At some
point there might be more generated HTML output or some IDE interface to
query the data.


	Makarius