Re: vocabularies

trybulec <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <[email protected]>
Dear Freek,

Freek Wiedijk wrote:

>>It is true, that the names of vocabularies are (mostly)
>>the same as the names of articles.
>>    
>>
>
>Precisely.  So making those names _exactly_ correspond
>seems a very minor change to me.
>
>  
>
The only exception that I know: the vocabulary 'ARYTM'. I do not know 
why it has such a name.

>>I cannot imagine how we could maintain MML with the
>>vocabularies glued in the articles.
>>    
>>
>
>Why not?  Instead of having two files foo.voc and foo.miz
>you would have one, but why does it matter how things are
>distributed over _files?_  And if you do _not_ want to make
>the names match up exactly, you could have dummy articles
>that _just_ have a vocabulary.
>  
>

What is the relation between foo.miz and foo.voc? How it happened that 
they have the same name?

When you submit a new article, you submit, sometimes, a new vocabulary. 
The Library Committee asks you
to assign the same name to the vocabulary as to the article. To simplify 
book keeping.

What is on foo.voc is often accidental. E.g. When attributes 'negative' 
and 'positive' were introduced in
ASYMPT_0, 'positive' was placed on the vocabulary ASYMPT_0.VOC, but not 
'negative', it already was
on the vocabulary ZF_REFLE.VOC.  After a revision the definitions of the 
attributes were moved to
XXREAL_0. But symbols are still on old vocabularies.

>I don't see the problem, sorry.  It is trivial to write a
>perl script that transforms a directory with separate .voc
>and .miz files into a directory in which the vocabularies
>are in included in the .miz files.  So to "maintain" MML
>one then could run that script, do whatever is needed for
>maintenance, and then run the inverse script.
>
>  
>
I like the first part. Why I should do the second?

Actually the vocabularies are kept in one file: MML.VCT. With the 
exception of private vocabularies, of course.

>But I don't see why for maintenance the vocabularies couldn't
>stay in the .miz files.  Can you explain?
>
>  
>
My mistake, if I restore MML.VCT, it will be no problem Only I do not 
like to do unnecessary job.

Without the preprocessing the problem is that an article may use a 
vocabulary that has the name of article that is processed later. What I 
have in mind that (without preprocessing) we should move symbols from 
one article to the other,
any time we change the order of processing.

Probably in such situation somebody would find that the vocabulary 
should be in a separate file. This would be a big discovery. And a big 
relief. :-)

Regards,
Andrzej
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.