[isabelle-dev] Functional type theory

[Makarius]

On Tue, 30 Jul 2013, Florian Haftmann wrote:

> The Isabelle checkpoints are gone:
>
> http://isabelle.in.tum.de/reports/Isabelle/rev/da1fdbfebd39
>
> This is reminiscent of how the West Goths resolved their problems at the
> Eastern Goths' customer clearance checkpoint:
>
> http://isabelle.in.tum.de/~haftmann/img/sledgehammer.gif

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
INCOMPATIBILITY.


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.


 	Makarius