Re: [mizar] Errors running mizf on irrat_1.miz

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

Dear Ryan,

the file

http://www.mizar.org/JFM/Vol11/irrat_1.miz.html

was written and verified using an old Mizar version, which is incompatible 
with the one you installed on your computer.

Verifiable files you can find on your computer in

/usr/local/share/mizar/mml

Best regards
Artur Kornilowicz


On Sun, 21 Oct 2012, Ryan Rusich wrote:

> 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