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

[mizar] Errors running mizf on irrat_1.miz



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