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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev