Re: [mizar] vocabullaries

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Adam,

>I think the 'vocabulary' (in singular) part would
>only be used when writing the article - after submission
>it could be transferred into mml.vct and removed from
>the article.

Why remove it?  It shouldn't hurt to keep the article intact.
Of course you also should have the mml.vct file.  But it
can be a _copy,_ can it?

I like the idea that if somewhere on an old disk you would
find an old mml directory full of *.miz files, that it
would be self-contained.

I even think I would like the vocabulary to also be part
of the .abs files.

>This procedure, however, would require importing (by
>default) a vocabulary named like the processed article,
>provided it exists in mml.vct. Keeping that part in the
>article seems useles as it's easier to use findvoc/listvoc
>to check the contents of a vocaulary rather than searching
>*.miz files.

Again, you can easily have it in _both_ places.  I like the
idea that you can easily see the article together with its
vocabulary, even if it's "frozen" in the MML.

>One minor disadvantage of keeping *.mi and *.voc as one
>file would be when working with a local library - at the
>moment several articles can share a local vocabulary and
>the change would require copying the 'vocabulary' stuff
>into several files.

I don't know about implementation issues, but doesn't it
seem natural to just have the name of one of them in the
"vocabulary" directive of the others?

To make that work you would need to generate a "local"
version of mml.vct to supplement the real mml.vct when
running miz2prel.  I guess.

Freek