Re: [mizar] Private DB

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Josef,

>The original problem was simplified import of other articles.
>Your suggestion now seems to be to solve that by [...]

But I have no problem with the way the notations work in
Mizar!  _That's_ not why I consider the Mizar imports to be
baroque (so baroque that you might even call it rococo!)

What I would like, for simplification of writing the environ, is:

1. To have the possibility to get _everything_ that's related
   to an article (vocabulary, notations, contructors,
   definitions, registrations, etc.) in one swoop.  So

	everything NAT_1;

   would be synonymous to

	vocabularies NAT_1;
	notations NAT_1;
	definitions NAT_1;
	constructors NAT_1;
	registrations NAT_1;
	theorems NAT_1;
	schemes NAT_1;
	definitions NAT_1;

   The idea is that this would not _replace_ the old style
   environ, but just be _extra_ for people like me who don't
   care to have a bit of irrelevant importing.  If there is a
   problem in a specific situation with this kind of overkill,
   the old style directives should also be there to give you
   fine control over what you get in case you need it.

2. To have the "extends" directive like we discussed.  So

	extends XBOOLE_0;

   would be synonymous to

	vocabularies TARSKI, BOOLE, ZFMISC_1;
	notations TARSKI, XBOOLE_0;
	constructors TARSKI, XBOOLE_0;
	registrations XBOOLE_0;
	theorems TARSKI, XBOOLE_0;
	schemes TARSKI, XBOOLE_0;
	definitions XBOOLE_0;

   Again, this directive should be _extra,_ for lazy people
   like me, and not replace the current system.  Let's be
   backwards compatible for optimal control.

3. To have a version of Mizar that has something like "irrths"
   built into the system in such a way that I don't need to
   write a "theorems" directive myself anymore.  I cannot
   count the number of times that I have added a reference to
   a lemma and then just got a _stupid_ error message (which
   one is it, *308?) that the theorems missed the
   corresponding article.  And then had to go up to the
   environ to add the article to the theorems directive, and
   then try to find the place again that I came from, and then
   wait for the check to rerun.  All lost time.  The system
   should be able to figure out by itself what theorems I use,
   no?  I mean, it's implicit in my article, isn't it?  So a
   simple implementation of this would be to just have the
   system update its list of which theorems the article needs
   (to be able to run accomodator) not all the time, but just
   when it gets this (*308?) error.

Of course the emacs mode could probably give you all this, by
"expanding" the everything and extends directives that I ask
for (and maybe also run Adams sortenv, just to keep things
tidy), and silently "fix" any problems that are caused by
missing theorems imports.

Freek