[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] referring to local files's constructors, theorems, etc
Hi Jesse,
On Mon, 19 Mar 2007, Jesse Alama wrote:
I'm working on splitting up a big MIZAR article into some smaller
articles. After I cut the original big article into pasted them into
a fresh article, I changed the various environments in the original
big file to the new smaller file. But when I try to verify the old
file I get errors like
*805: Cannot find definitions file
and
*806: Cannot find theorems file
I've run the new file successfully through the verifier; it looks like
something else is needed. How can I get rid of these errors?
Indeed, you need something more than just verification of your articles:
if you want to split your article into several parts which
require one another, you have to create a so-called local database using
the 'exporter' tool (see http://mizar.org/system/exporter.html). But
instead of calling it by hand, you should use the macro 'miz2prel' with
one argument being the filename of your article to be included in the
database. This produces a subdirectory 'prel' containing the database
files. Having exported an article, you run Mizar again for all dependent
articles and then your errors should disappear.
BTW, if you're using Emacs mode for editing your article, then just go to
<Mizar> -> <Other Utilities> -> <Miz2Prel>.
Best,
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/
======================================================================