Re: [mizar] vocabularies

[trybulec <trybulec@math.uwb.edu.pl>]

Josef Urban wrote:

> On Tue, 6 Jan 2009, trybulec wrote:

> Side note: If you use Emacs, use Alt-/ for dynamic completion of such 
> identifiers. For example, if you want to write "SQUARE_1", and have 
> "SQUARE_1" already in the environment, then only type "SQ" or "SQU" 
> and then press ALT-/ to complete. If there is no dynamic completion, 
> something is wrong (you mistyped or the identifier is nowhere in the 
> article yet).
>
> One possible additional check (in Emacs) would be to watch if the 
> added identifiers are in mml.lar or the current environment after 
> entering "by.*;" . Probably not a big deal.
Better to check DB for the #.THE file. I quite often work will partial 
DB, so checking MML.LAR does nor help.

> Provided that (using such mechanisms) you will never mistype here, 
> Freek's complaint wins (I think his problem is fairly frequent too). 
> But Freek's complaint can be also dealt with automagically in Emacs 
> :-) (i.e. the environment directive appended).
Thanks for the explanation. I should get more accustomed with the Mizar 
mode in emacs. I believe it is a proper way
to deal with the preprocessing.

> > 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.
>
>
> Just one more pass in a multipass compiler :-). If white char is 
> strictly required before and after "by" and "from" (I am not sure 
> now), then a very cheap pass. But I would do a check against mml.lar 
> (plus local db) before running accommodator, and complain if there is 
> a typo instead of accommodating.

No so cheap. One cannot use a standard PARSER (lexical analysis 
impossible), so we need a special version of
PARSER and moreover a special version of SCANNER (TOKENIZER). One bloody 
program more to maintain.

The "division of labor " is now clear. The ACCOMMODATOR processes the 
Environment Declaration and
creates the environment of the article, an ad hoc little theory, sort of.

Then the VERIFIER (RELPREM, EXPORTER, whatever) process the article in 
the given environment. I would not
change it.

I am not against interactive help with creating the Environment 
Declaration. I am definitely pro.It is much needed But it should not be 
mixed with other utilities.

Regards,
Andrzej