Re: [mizar] vocabularies

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

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