Re: [isabelle] AFP and Library




On 30/08/2017 23:40, Makarius wrote:
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.


As long as this is transparent, you are of course welcome to optimize "isabelle build" for tasks like the AFP. Everything that involves changes to the AFP needs to be discussed first.

Tobias

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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