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



On 02/20/2012 05:19 AM, Makarius wrote:
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.
I'm referring to this thread.

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-February/msg00092.html

(Sorry I had Lukas' answer (which contains the above link) already on my machine before it arrived at the list but did not notice the difference at first.)

cheers

chris


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.