Re: [mizar] vocabularies

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

Dear Andrzej,

>To move a symbol from a vocabulary A to a 
>vocabulary B
>is a lot of work. At least:
>1. To look to all 1000 or so articles and change if necessary the 
>'vocabularies' directive.
>2. To modify data for JFM
>3. To check if parsing is still correct, of all MML. Actually it may be 
>worse, the parsing is correct
>but the meaning of the article has been changed.
>and probably more.

But it is exactly the same in the current situation (where
the .voc files are not in the .miz files), if you would
choose to move a symbol between vocabularies!  I don't
see why this is an argument to not have the text of the
vocabularies be part of the .miz files.

I you would change Mizar in such a way that all vocabularies
would be automatically available in all articles, so that
there wouldn't be a vocabularies directive in the environ
anymore, then I agree that it would be strange to have them
be part of the article.  _Then_ it would be natural to have
them be part of a global file mml.vct.  But is that where
you want to go to, eventually?

>What is the natural place for the attribute symbol
>'negative'?

ZF_LANG, apparently :-)  (Or maybe ASYMPT_0, as that's where
"positive" seems to be :-))

>I am ready to do a lot of work, if necessary. Why I should
>do more work, if it is not necessary.

But I don't see why anything would be more work if the
vocabularies would be part of the .miz and .abs files.
I'm just asking for a slight redistribution of existing
text among files, not to significantly change anything.

To repeat myself (and maybe I just should shut up, as it's
clear that you won't follow this suggestion of mine): what
does it matter where the text of the vocabularies is stored
in the file system, as long as the way you use the system
stays essentially the same?

Maybe I'm missing something in this discussion, but then
I don't see what.

>Nothing to gain, only troubles.

No, no troubles either!  And the gain would be that you just
have one file for your article, instead of two, which is much
simpler.  Also no "dict" directories would be needed.  _And_
MML would be more "self contained".  Currently you need the
mml/*.miz files _and_ the mml.vct file to make sense of it.
Then you only would need the stuff in the mml directory.

>We have now more flexible system keeping the lexical
>resources separated from articles.
>It works pretty well, why to changed it?

Ah well.  Leave it the way it is, then.  But don't ask me
not to tell people that I find Mizar a bit rococo :-)

Freek