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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
