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