Re: [mizar] vocabularies

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

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