[isabelle-dev] typrep?

[Florian Haftmann]

Hi all over there,

some comments on my behalf:

a) The Typerep theory if used by Imperative_HOL, but this is *not* its
only application; it is also used for evaluation using code generation
(value [code]) -- indeed, I added this immediately after the 2008
release in order to gain some experience how this machinery works and
which problem it raises.

b) Beside "typerep" and "size", there are also "itself" and "eq";
similar mechanisms are also used for datatype realizers and sledgehammer.

c) I agree with Alex that the reason why only typerep so far caused one
problem is that typerep is bootstrapped rather lately because it needs
lists, and thus you might run into problems if you rearrange the HOL
thygraph.

d) I accept that the behaviour Amine has encountered is difficult to
trace, but -- we should have no illusion: *developing* HOL is more
delicate than *using* HOL anyway.  For this reason we have the
advertised entry points Base, Plain, Main, Complex_Main which provide a
consistent setup of packages, whereas using other HOL theories directly
is branded as "use at your own risk" explicitly.

e) Of course there still remains the burden for HOL developers to find
an appropriate thygraph layout, but this has never been trivial, typerep
notwithstanding.  "Bad" layouts can even give raise to mysterious
non-functional discrepancy, e.g. the recent replacement of Univ_Poly by
Polynomial which does not need lists anymore produced a significant
speedup in building the HOL theories (perhaps due to a different
sledgehammer situation).

f)
> I, for one, am rather alarmed at the hurdles that Amine was forced to overcome to do a simple merge of two theories. Even before the typerep-related problems, merging Isabelle theories was already difficult enough! I think that merging theories is one of Isabelle's most serious weaknesses, and it has prevented many users from being able to borrow, share, and build upon each other's code. (Witness how little re-use of code there has been among AFP entries, in spite of the recommendation in the submission guidelines, "It is possible and encouraged to build on other archive entries in your submission.") 

I see the point that failing merges are hard to trace (if not impossible
without guidance of an expert), but so far I did not have the feeling
that this would be the main obstacle for library developement.

Regardless of this discussion, it would be interesting to hear about
such failures in order to try to amend them.

Hope this contributes to clarify the situation,
	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090121/ae655db0/attachment.sig>