Re: vocabularies

Freek Wiedijk wrote:

>>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.
>
>  
>
The "big" difference is in the fact that I am not pressed to move
 a symbol to another vocabulary if I changed the order of processing.

>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?
>
>  
>
It is no feasible to have all vocabularies available to all articles. 
The reasons:

1. a symbol that has the form of an identifier may be used in an article 
as identifier
    (if its vocabulary is not in the environment)
2. composite cymbols like '+*', '{}.' may cause a differnet parsing when 
they become available.
3.  some symbols are just traps. It is well know that one has to be 
careful using 'c='
  if one writes
                                a \ c= a \ b
'c' is not recognized as an identifier. Less known is the symbol for 
Cartesian product
                                    [x]
(the vocabulary CAT_4) I wrote a scheme with something like

            P[x] & P[y] implies  ....
after adding the vocabulary CAT_4 I got wrong parsing
       P [x]
and a syntactic error.

So, maybe we should redistribute symbols between vocabularies.

A huge vocabulary with common symbols (HIDDEN resembles it, only it is 
not huge; I do not like it, because
it is not controlled by the user).

One symbol vocabularies for such symbols like
     [x]
or
      x.
in ZF_LANG. (Well, we rarely use the identifier 'x' for functions).

>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.
>  
>

Under the assumption that we restore MML.VCT, you are right.

>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?
>  
>

I appreciate the discussion, it made some problems more clear for me.

>Maybe I'm missing something in this discussion, but then
>I don't see what.
>
>  
>
Let's try to fix 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 :-)
>  
>

Never crossed my mind.


Merry Christmass,
Andrzej