[mizar] Fwd: free ultrafilters

[Josef Urban <josef.urban@gmail.com>]

I am really wondering if the Mizar community will go open-source in my
lifetime, or if this is the kind of Keynesian "long-run scheme" whose
(so difficult!) completion will outlast everyone (including Mizar
itself).


---------- Forwarded message ----------
From: Freek Wiedijk <freek@cs.ru.nl>
Date: Fri, Dec 11, 2015 at 11:39 AM
Subject: Re: free ultrafilters
To: Nicolas Ratier <nicolas.ratier@femto-st.fr>
Cc: Josef Urban <josef.urban@gmail.com>


Hi Nicolas,

>I would like to ask you some questions about Mizar.
>
>1/
>I made a OCaml parser of the Mizar grammar.
>Result :
>$ ocamlyacc -v mizarparser.mly
>2 rules never reduced
>216 shift/reduce conflicts, 323 reduce/reduce conflicts.
>(Many precedence rules are not defined/written,
>but it doesn't explain the huge number of conflicts).
>What tools they used to parse Mizar grammar ?

It's a handwritten parser, programmed in Pascal.
It's "semantic", in the sense that in certain places the
system needs to know what the arity of type constructors
("modes") are.  For instance when you write:

for f being Function of A,B, x,y being Element of A holds ...

then the system needs to know how to cut up the "A,B,x,y"
into the arguments of "Function" and the variables with type
"Element of A".  It think.  When "B" is not a variable
that's in scope, I guess those variables with then be
"B,x,y", and the type of f will be "Function of A"...

The expression parser is easier than that, but also not
something that (I think) would be easy to parse with yacc.

See also <http://www0.cs.ucl.ac.uk/staff/ucacjig/papers/parsing.ps.gz>
and <http://www-old.newton.ac.uk/preprints/NI12011.pdf>.

>2/
>Do you think that it would be possible to translate Mizar
>in OCaml in not so much time? I cannot figure if Mizar
>is a very complex program or if it is the library MML which is
>really valuable.

It is not a _very_ complex program, but it certainly won't
be a small project, especially if you want to have it be
exactly compatible with the current system (which is needed
if you want to be able to process the MML).  The Mizar
group has been working on a C (C++?) version of Mizar,
but I don't know what the state of that is.

>3/
>I don't understand why Mizar is so "secret" ... ?
>Everything is copyrighted (why ???)
>Only polish people have a membership (but you).
>
>It seem so difficult to become a Mizar membership
>Here is a copy-paste from there web site :
>
>=========================================
>In order to obtain the ordinary membership of the SUM one must:
>
> * use the Mizar language <http://mizar.uwb.edu.pl/language/> actively,
> * be introduced by two members of the Association (charter members or
>   ordinary members who belong to the Association for no less than
>   three years),
> * obtain a positive decision of the Board of Direction of SUM.
>
>========================================
>
>I cannot believe it !!!
>And it is only for ordinary membership !!!! Imagine
>what you have to do to become a extraordinary membership
>(I joke of course)

:-)  If you're interested in this aspect, you should talk
to Josef Urban (I'll CC him).  I think this is mainly
historical, Andrzej Trybulec felt strongly about this,
and maybe even outdated.

Freek