Errors running mizf on irrat_1.miz

Ryan Rusich <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <CAEqsRmMRApO_3EHNJg5P62HfkJQMKbAzb8W4G9TZizXKofxa=A@mail.gmail.com>
Dear Mizar Users, I am attempting to get Mizar installed and run some
example *.miz files.

I have installed from the source mizar-7.14.01_4.182.1147-i386-linux.tar:
on a CentOS system with the following kernel:
2.6.18-308.11.1.el5PAE
I have followed the README, contained in the archive listed above.

One of the examples I tried to run through mizar I located from:
http://www.cs.ru.nl/~freek/100/mizar.html
which directed me to:
http://www.mizar.org/JFM/Vol11/irrat_1.miz.html

To test,
I created a text and dict directory locally, then placed an instance of
irrat_1.miz in the text directory.
I next ran the following command in that text directory:
mizf irrat_1.miz

This issued the following message:
$ mizf irrat_1.miz
Make Environment, Mizar Ver. 7.14.01 (Linux/FPC)
Copyright (c) 1990-2012 Association of Mizar Users
**** 3 errors detected
All three errors were listed as *201 errors, all located in the environ
section of the file. I have listed them.

vocabulary INT_1, ARYTM, SEQ_1, FINSEQ_1, RAT_1, POWER, FILTER_0, SQUARE_1,
::>       *210

notation XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, INT_1,
::>     *210

 clusters RELSET_1, XREAL_0, SEQ_1, INT_1, NEWTON, NAT_1, MEMBERED,
ORDINAL2,
::>     *210

Here is the description of this particular error message(inserted at the
bottom of irrat_1.miz)
::> 210: Wrong item in environment declaration

I found the same behavior when I installed mizar on an Ubuntu machine and
tested irrat_1.miz in the same manner. On other tests I have run into
similar errors or there appears to be unresolved dependencies in files as
well.

---------------------------------------------------------------------------------------------------------
Perhaps I am missing some fundamental technique on how to run the software?

Before I work on my own articles, I want to ensure I have a correctly
functioning
version of mizar.
----------------------------------------------------------------------------------------------------------

Thank you for your time.

Kind Regards,
Ryan Rusich

P.S. I have also used the following references in my initial study of mizar.
"Writing a Mizar article in nine easy steps" by Wiedijk
http://www.cs.ru.nl/~freek/mizar/mizman.pdf
"Mizar in a Nutshell" by Grabowski, Kornilowicz and Naumowicz
http://jfr.unibo.it/article/view/1980/1356
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.