Re: [mizar] vocabularies

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

Dear Andrzej,

>Maybe more important is that you should first run PARSER
>(for the Text Proper), to generate a file for the
>ACCOMMODATOR (maybe incorrect) and then to run the
>VERIFIER. Clumsy.

Of course you could also have a _separate_ tool that would
find all theorems used by your article, and then update the
article if necessary, by adding missing references to the
theorems directive.

You could then add that to mizf at the start.  So mizf then
would be:

(1) run that tool
(2) continue with the current mizf

If the article was changed because the theorems directive was
extended by the tool, accomodator would be run by the second
step (so yes, then you parse the article before _and_ after
accomodator), but that's unavoidable.  If you had updated the
theorems directive yourself, accomodator would be run too.

Maybe it's in some sense clumsy to do it like this, but
getting irritated now and again (in my case: quite often) by
having to change the theorems directive when in the middle
of working on my formalization is clumsy too.  (I have to
go to the environment, change stuff there, reflow the lines
if necessary to get under the 80 column limit, and then
somehow get back to where I was working.  It's distracting.
And, as I said, often I forget about the theorems directive,
and get irritated by the error message as well.)

So having a tool that messes with your article (if only with
the environment) sounds a bit scary, but error messages
are inserted in the article as well, so it's not a very
big change.

Freek