Email Gateway (Aug 18 2022 at 14:33): Email Gateway (Aug 18 2022 at 14:33):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Seconded!
I've been going on about this for years, but haven't been giving it high enough priority.
Gerwin
Email Gateway (Aug 18 2022 at 14:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
A feature that I often miss, especially considering namespace pollution
problems. One of the top-candidates on my wish list
is something like import-qualified, giving the user control over what
symbols (and syntax) will be loaded into the toplevel-namespace.
This is a misunderstanding which exhibits the source of the problem:
syntax is not bound to namespaces but always global, which makes
pollution pervasive (c.f. the funny (no_)notation declarations for inf
and sup in the HOL theories -- an Isabelle joke...). We need finer
control over syntax here.
Currently, the hide-command allows one to hide
private symbols, but the other way round would be more comfortable.
I do not seed this demand as urgent: given that theory developers have
thought carefully which symbols ought to be hidden / qualified, the user
is always free to hide additional symbols when needed.
If users want hierarchical module names, why don't we (the Isabelle
developers) just implement that feature?
I agree that this is desirable. But I suppose we first should find a
way to replace the rather archaic session concept by something which is
less driven by building descriptions in IsaMakefiles and ROOT.MLs, but
by the implicit structure of hierarchies.
A somehow related question is how to treat relative imports. I recall
there has been (still is?) much debate on this in the Java and Python
community, and this has to be considered carefully (maybe inspired by
Scala!?).
Tapping yet another barrel... ;-)
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
A related issue: we have to encourage ourselves to factor out generic
formalisations from applications, as Tobias pointed out. From my
perspective the four major obstacles are:
difficult to tinker with the bootstrap theories above Main.thy, even
for developers (a typical candidate would be List.thy);
incoherence and duplication in existing theories themselves, which
make it difficult to decide what "the" way for contributed things
actually is.
But this leaves still room for contributions to HOL/Library or separate
AFP articles. It would be interesting to hear experiences and comments
from users who have tried to factor out library theories from their
applications -- successes and failures.
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:35):From: Makarius <makarius@sketis.net>
Well, I did give it a high priority, but it is technically very difficult.
In principle we already have sufficient infrastructure to control
visibility, or limit all kinds of "declarations" (syntax, hints to proof
tools) to a certain scope. It is all part of the "local theory"
infrastructure.
Unfortunately, we are still stuck halfway in localizing everything -- this
refers to specification packages in the main library (datatype,
nominal_datatype etc.). Then the toplevel theory context can be treated
as just another local theory target, and benefit from additional control
over when and where declarations actually hit the user context.
I am in the middle of a major effort to work towards that again.
Nonetheless, it will take several more rounds to get there eventually.
Even worse, I recently see tendencies in user tools to forget about proper
locality and go back to global operations on the bare metal of the raw
theory context.
Makarius
Email Gateway (Aug 18 2022 at 14:35):From: Makarius <makarius@sketis.net>
Better use 'notation' / 'no_notation' which perform static checking of the
term constants involved. The more primitive 'syntax' / 'no_syntax' is
only needed for very special syntax table manipulations.
Makarius
Email Gateway (Aug 18 2022 at 14:35):From: Makarius <makarius@sketis.net>
There are already well-established concepts of long names, name bindings,
naming context, name spaces, which are used everywhere except for the
theory database. So one merely needs to make theories conform to the
established scheme, and somehow link up with the theory loader.
All of this is completely non-trivial.
Nonetheless, it should happen eventually, and without putting the system
into an undefined state.
Makarius
Email Gateway (Aug 18 2022 at 14:36):From: Gerwin Klein <gerwin.klein@nicta.com.au>
On 22/02/2010, at 8:10 PM, Florian Haftmann wrote:
A feature that I often miss, especially considering namespace pollution
problems. One of the top-candidates on my wish list
is something like import-qualified, giving the user control over what
symbols (and syntax) will be loaded into the toplevel-namespace.This is a misunderstanding which exhibits the source of the problem:
syntax is not bound to namespaces but always global, which makes
pollution pervasive (c.f. the funny (no_)notation declarations for inf
and sup in the HOL theories -- an Isabelle joke...). We need finer
control over syntax here.
Yes, we do.
We don't need to do everything at once, though. We'd still be in a well-defined, better state if we could just treat normal names (thms, consts, types) in theory name spaces.
Currently, the hide-command allows one to hide
private symbols, but the other way round would be more comfortable.I do not seed this demand as urgent: given that theory developers have
thought carefully which symbols ought to be hidden / qualified, the user
is always free to hide additional symbols when needed.
This requires the user to know everything in the libraries (and track all syntax changes over library versions). Much better to be able to import only what you want.
In our project we have really bad cases of name space pollution (three large specifications describing the same thing, names do get scarce quickly). The conceptual problem is long solved in other languages. We "just" need to implement one of the solutions.
If users want hierarchical module names, why don't we (the Isabelle
developers) just implement that feature?I agree that this is desirable. But I suppose we first should find a
way to replace the rather archaic session concept by something which is
less driven by building descriptions in IsaMakefiles and ROOT.MLs, but
by the implicit structure of hierarchies.
I see that as a fairly orthogonal problem (not that it shouldn't be addressed at some point). The sessions really only govern what theories get loaded when. All actual dependencies and data are tracked on the theory level by Isabelle already anyway. I'd rate proper name spaces a much higher priority.
A somehow related question is how to treat relative imports. I recall
there has been (still is?) much debate on this in the Java and Python
community, and this has to be considered carefully (maybe inspired by
Scala!?).
In terms of name space handling, I so far like the Haskell model best. This is something that can easily be discussed and tweaked, though (almost as hard as concrete syntax ;-))). The real problem will be down at the technical end as Makarius writes.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 14:48):From: Tobias Nipkow <nipkow@in.tum.de>
This theory provides functions for finding the index of an element in a
list, by predicate and by value.
http://afp.sourceforge.net/entries/List-Index.shtml
Above I have intentionally not used the word "article" but "theory" to
emphasize that this is a small contribution (a single theory of modest
size) - but a reusable one! I would like to use this opportunity to
remind readers of this list of the purpose of the AFP:
"The Archive of Formal Proofs is a collection of proof libraries,
examples, and larger scientific developments."
At the moment the majority of contributions are large (sometimes
impressively so), monolithic developments. Very rarely are parts of such
developments reused elsewhere. That is, the library aspect is
underdeveloped. The above theory "List Index" used to be hidden in the
article "Jinja is not Java" and I have (after 5 years!) finally gotten
around to making it a separate contribution.
This is a call for reusable AFP entries. I am sure many of you have such
theories hidden away in their drawers (or their AFP entries): Do take
the time to polish and submit them to the AFP (or refactor some existing
AFP article), for the benefit of the whole community (and your fame).
Don't think publication, think reuse!
Sorry about getting carried away ;-)
Tobias
Email Gateway (Aug 18 2022 at 14:48):From: Tobias Nipkow <nipkow@in.tum.de>
My immediate plea is for modular library components. Having those as
top-level entries dramatically increases the likelyhood that they are
reused.
But you are quite right: Hackage offers some things worth emulating:
Tobias
Simon Winwood schrieb:
Email Gateway (Aug 18 2022 at 14:48):From: Peter Lammich <peter.lammich@uni-muenster.de>
Tobias Nipkow wrote:
A feature that I often miss, especially considering namespace pollution
problems. One of the top-candidates on my wish list
is something like import-qualified, giving the user control over what
symbols (and syntax) will be loaded into the toplevel-namespace.
Related to this would be the possibility to specify the public interface
of a theory. Currently, the hide-command allows one to hide
private symbols, but the other way round would be more comfortable.
Peter
Email Gateway (Aug 18 2022 at 14:49):From: Simon Winwood <sjw@cse.unsw.edu.au>
Perhaps a useful model to emulate is Hackage. For those who don't know,
hackage is a website (similar to the AFP) for hosting haskell packages. One thing that
makes it so useful is the cabal utility --- somewhat like debian's apt tool --- which
allows you to download a package and all its dependencies automatically. This seems
to encourage both reuse and participation.
Whether or not this would work for the Isabelle community is debatable --- the
the haskell community is much larger. Having said that, we might be able to co-opt
some of the tech used in cabal and hackage ...
Simon
Email Gateway (Aug 18 2022 at 14:49):From: Brian Huffman <brianh@cs.pdx.edu>
If users want hierarchical module names, why don't we (the Isabelle
developers) just implement that feature?
The implementation wouldn't involve much:
Make the dot "." a legal character in module names.
Define a new mapping from module names to filepaths, so that
"imports A.B.C" makes Isabelle load the file "~/A/B/C.thy", where "~"
is filled in with some directory from the search path.
The hard part would be social, rather than technical: Deciding how to
organize and populate the hierarchy. But we wouldn't have to switch
over everything at once---we could flesh out the hierarchy gradually,
with input from the user community, and move libraries to their new
places in the namespace one at a time. I think this would work, and
solving the problem of module name clashes would remove one big
obstacle to sharing Isabelle libraries.
Email Gateway (Aug 18 2022 at 14:49):From: Brian Huffman <brianh@cs.pdx.edu>
Yes!
Besides the flat module namespace, I think that syntax clashes are the
other big obstacle to sharing Isabelle libraries. I have experienced
this problem from both sides.
As a user importing other Isabelle libraries, I have often been
constrained in the choice of syntax to use for my own theories,
because so many useful bits of syntax are already taken by something
in Isabelle/HOL. For example, if I use "_ [_ / _]" as a notation for
substitution in one of my own theories, this causes ambiguous parse
warnings, due to clashes with the List library. This is especially
annoying when my theory does not use lists at all!
As an implementer of Isabelle libraries, adding special syntax for
constants is quite worrisome: What if the end-user of this library is
already using the same syntax for something else? This is the reason
why RealVector.thy doesn't define the standard "||x||" syntax for
"norm x" (I tried adding it once, but it clashed with another
library), and Library/Inner_Product.thy doesn't define an infix-dot
notation for the inner product.
Of course, I can always define nice syntax to use within the library
itself, and then use "no_syntax" at the end to avoid potential clashes
with user theories. But some users might actually want to use my
syntax! It seems silly to have the library decide for all users
whether or not some bit of syntax will be visible to them. Obviously,
this choice should left to each user of the library, as Peter
suggests.
Last updated: Apr 16 2024 at 20:15 UTC