Re: [isabelle] [isabelle-dev] Some missing setup for function package in combination with Option-type



On Fri, 17 Feb 2012, Christian Sternagel wrote:

Concerning Tobias original mail (on small AFP entries): Strange how one can forget mailing list discussions that were actually read with great interest ;). What is the current state w.r.t. the discussion that followed in 2010?

Can you point to the specific thread? These are recurrent topics, and I have commented on them many times with varying details and focus.


IIRC, the points were roughly
- module name spaces

This probably means several things:

  (1) clear indentification of theory files in the file-system
  (2) qualified theory names
  (3) ways to include theories without flat name space merge

- visibility of syntax

The latter is probably closely related to (3), and there is some chance
that the existing concept of syntax_declaration in the local_theory department will address that.

Point (1) is addressed to some extent in official Isabelle2011-1 when using the Isabelle/Scala document model, currently mainly via Isabelle/jEdit. Here nodes are identified by full file names, so the implicit collapse to theory base names is avoided. Thus it is already possible to load most of AFP into one editor session without interfering (which is only fun on 32 GB hardware). Using separate theories Foo/Array.thy and Bar/Array.thy together requires some further reforms that are not immediate.

Point (2) sounds easy, but is hard due to many entrenched customs about name space usage in Isabelle. When the concept first occurred in 1998 it was already clear that the common format of long names A.c (or A.b.c with locales) is only accidental. Nonetheless, existing tools occasionally depend on that. It will take more time to sort out all improper uses of long names and name spaces. (Just some days ago I've convinced myself that at least the use of "intern" is mostly right in the existing code base for the next Isabelle release.)


- installing entries (+ dependencies; something like cabal for Haskell)

What means "installing"? Once we have a proper session specification in the source trees (not ROOT.ML nor IsaMakefile) you merely point to such points in the file space without "installation". Or did you mean installation of so-called Isabelle components?

Dependencies are already managed pretty well by the Isabelle/Scala layer. I hope people will dispose their private perl/python approximations at some point. It is only one more step to unify this with the batch mode, and discontinue the old usedir stuff (which is from the mid 1990-ies). It will mean that there is only one way to process sources, without surprises about different flags for skipping proofs etc. -- but sometimes this behaviour is actually exploited, hindering such reforms again.


Is there any way in which non-developers (like me) could contribute to anything of the above?

Part of the problem is the adhesion of many power users to extremely old versions of Proof General / Emacs. De-facto I am still the main maintainer of Proof General 3.x and 4.x, with lots of Emacsen on Linux, Mac OS X, Windows. At the same time I am trying to get rid of the TTY/Emacs regime for 4 years already.

It would help if the adherents to Proof General would somehow organize themselves to take over the responsibility to maintain it with all consequences.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.