Re: [isabelle] AFP and Library



On 28/08/17 15:35, Makarius wrote:
> 
> At some point, "isabelle build" could use the persistent timing
> information from the database to make better scheduling of big builds,
> including adhoc changes to the actual session graph (e.g. changing
> parent sessions vs. session imports).

Some more notes on this.

The present reform of session-qualified theory names in Isabelle2017
still allows old-fashioned unqualified imports from existing parent
session images. It eases the upgrade of existing project sources, but it
means that the parent session structure still has an impact on the
theory name space.

Right after the Isabelle2017 release we can get rid of that, and parent
sessions vs. imported sessions (keyword 'sessions' in the ROOT) become
interchangeable -- as far as logical theory names are concerned (not the
time for loading theories).

This opens many possibilities to rearrange things, either statically in
the ROOT files, or dynamically by a smarter version of "isabelle build".
For example, all AFP sessions with < 30s runtime could be built in one
big ML process, for improved parallel performance and to avoid loading
the base session many times.

There are many more possibilities, especially with full timing
information of all sessions, theories, commands available to the build
process.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.