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