[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] vocabullaries

Hi,

On Tue, 2 Dec 2008, Freek Wiedijk wrote:


Of course _I_ always want the vocabulary files to be part
of the articles.


Are you really serious about it?


Yes!  Completely serious.

I think I would like the articles to have three parts:

	environ
	  ...
	vocabulary
	  ...
	begin
	  ...

So there wouldn't change too much, but there would be
just one file that one would need to work on, and one
"name space" that would be shared for naming both articles
and vocabularies.
I also like the idea of "glueing together" the *.miz and *.voc files - it's the way it is now. 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. 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.
One minor disadvantage of keeping *.mi and *.voc as one file would be when working with a local library - at he moment several articles can share a local vocabulary and the change would require copying the 'vocabulary' stuff into several files. But to me it's a minor problem, since this is exactly what we usually do with the environment, anyway. 


Regards,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================