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
This archive was generated by a fusion of
Pipermail (Mailman edition) and