[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

[Florian Haftmann]

Dear all,

last week I spent some considerable time and energy to get rid of the
locale (open) feature,  which was in most cases straight forward and
trivial -- except the issue of MicroJava, Jinja, JinjaThreads.  I think
it is worth to document my experiences here for the future.

The three obfuscating issues were:

A) Archaic, hardly readable and fragile proof techniques:
  * unfolding definitions of predicates over logical formulae instead of
    proper intro/elim-rules
  * long apply-Scripts with sometimes obscure tacticss

B) Naive use of locales (instead of proper interpretation):
  * somehow arbitrary mixed explicit locales and simple predicates
  * free-floating use of uninterpreted global rules from locales
  * use of "defines", where definition etc. would be appropriate

C) A lot of forked (but not shared) theories in MicroJava, Jinja,
JinjaThreads.

Of course, all these are due to historic reasons, layers of increasing
state of the art built on top of each other.  Anyway, concerning C),
IMHO in the future we should try harder to avoid such duplication by
distilling reasonable libraries out of large-sized projects.  E.g. these
projects contain independent developments of semilattices, work which
would fit more appropriately in HOL-Algebra and then could simply be
re-used.  Such shared libraries would greatly increase the motivation
and benefit for keeping them technically at the height of the day than
such (superficially) "specialized" and "adapted" theories scattered over
different projects.

	Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20080728/c6c73631/attachment-0002.vcf>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20080728/c6c73631/attachment.sig>