[isabelle-dev] Functional type theory
makarius at sketis.net
Wed Jul 31 13:57:02 CEST 2013
On Tue, 30 Jul 2013, Florian Haftmann wrote:
> The Isabelle checkpoints are gone:
> This is reminiscent of how the West Goths resolved their problems at the
> Eastern Goths' customer clearance checkpoint:
This joke is too subtle for me to understand.
My NEWS announcements are lagging behind the pushes. The relevant one for
above is this:
* Type theory is now immutable, without any special treatment of
drafts or linear updates (which could lead to "stale theory" errors in
the past). Discontinued obsolete operations like Theory.copy,
Theory.checkpoint, and the auxiliary type theory_ref. Minor
Many years ago, the theory stamp size was considered a problem: there used
to be approx 20 stamps with quadratic subset check, although it often
turned out as linear.
In 2005, I've made this already much better: a fully balanced table with
a single (!) logarithmic lookup for the subtheory check. Stamps only at
theory node boundary.
Around 2008 many more checkpoints were introduced for parallel proof
checking. Later checkpoints were made at every local theory transactions.
Making a few performance tests recently revealed that fully immutable
theory values merely increase the stamp size by a factor of 5, leading to
approx. 100000 in main HOL and 300000 in JinjaThreads, with hardly any
measurable impact of performance. It leads to approx. 20 table lookups in
every kernel inference, just as in acient times.
So this issue is now on the historic list of "premature optimizations that
complicate code", namely that of the kernel. Even just practically, the
"stale theory error" has probably wasted more time of tool developers that
it saved CPU time.
More information about the isabelle-dev