[isabelle-dev] Issues with "interpretations"

[Makarius]

On Wed, 2 Apr 2014, Jasmin Christian Blanchette wrote:

> My work on (co)datatypes and my desire to move "Quickcheck_Narrowing" 
> out of HOL and into Library have lead me to discover several issues with 
> the interpretation mechanism ("Pure/interpretation.ML") that is used to 
> hook into various modules (e.g., the "size"-generating extension to 
> "datatype"s). I will summarize my findings below. It might well be that 
> this is already (at least partially) known to some of you.
>
> In the following, I will talk concretely about datatype and their 
> various hooks (size, Quickcheck random, Quickcheck narrowing, etc.), but 
> the same issues can arise in principle with all the other 
> hooking-mechanism based on "Pure/interpretation.ML".

[...]

This is indeed a careful study of the possibilities what can go wrong.

We have accumulated various funny hooks over the years to "saturate" 
theory content in a post-hoc fashion, but they are just "features of last 
resort" to avoid certain bootstrap problems.  If there is a way to do 
without any such magic, it would be the better solution.


> 1. As long as we define new interpretations (hook types) in the HOL
>    image, we can reorganize the imports to avoid the evil scenarios.
>    Problems arise when users define their own interpretations.

IIRC, this is the original intention and still the state of the art in 
Isabelle/HOL bootstrap (but I could not follow its details in recent 
years).  So interpretation is just an odd tool to do the boostrap somehow, 
but not for regular user-space theories outside main HOL (notably 
HOL-Library).

The inevitable "knot" below theory Main was one of the reasons why it was 
declared a black box to end-users many years ago.  Theory Main is 
delivered for general import, but anything below it is conceptually 
private (although the system does not check nor prevent accidental 
access).


> 2. In particular, moving "Quickcheck_Narrowing" outside HOL and into
>    Library raises this issue in JinjaThreads. I will see if I can
>    reorganize the imports.

So this is a clear counter indication.  Unless Quickcheck_Narrowing is a 
big hulk getting in the way inside Main HOL, I would just leave it there.


> 3. Despite the failure with Scenario 3, the way "size" does things looks
>    superior to the other approach, and I'm tempted to standardize on
>    this for the old-style and new-style datatype hooks. I have patches
>    ready already (cf. testboard).

I guess that is now changeset 32e0da92c786, which is relatively small and 
conservative in the sense that slightly odd workarounds from the past are 
merely continued.

Thus it is reasonably easy to change the direction later.  Sign.root_path 
is working against the present plan to introduce qualified theory names, 
but that is on hold anyway, for > 10 years.


> Please stop me if you disagree.

Oddly we've had this situation about three times within just a week. It 
does not make any sense to broadcast an announcement of a presumably 
non-obvious changes and push within a few hours or days.  Realistically it 
requires 2-3 weeks of general permeation, probably also with some 
intermediate reminders.

Our usual procedure is that someone who can claim experise on a certain 
area just pushes a change, and potential discussions can come afterwards. 
(Doing something by analogy to existing approaches inherits the expertise 
of the guys who did it in the past.)

If somethings is unclear and no expert around, there will be a lengthy 
discussion with many people who have some partial knowledge, and usually 
unclear conclusions.


 	Makarius