Re: [isabelle] New AFP theory: List Index

On Mon, 22 Feb 2010, Gerwin Klein 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.


I've been going on about this for years, but haven't been giving it high enough priority.

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.


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