Re: [mizar] Question on Mizar grammar

[Michael Nedzelsky <MichaelNedzelsky@yandex.ru>]

Hi Josef,

 At the end of http://www.mizar.org/language/syntax.html there is a string:
  Done with grammar2thtml.xsl

It seems that the syntax.html was built from some XML-file for Mizar grammar.  
Is it XML-file still available anywhere?

May be this question must be addressed to Grzegorz Bancerek, though I hope he 
use this mail list too. :)

> looks like a bug, the grammar version at
> http://mizar.org/language/pages/predicate-definition.html#predicate-definit
>ion with Correctness-Conditions instead of [ "correctness" Justification ";"
> ] seems more correct.

The version was last modified: June 26, 2000 and seems more correct than
both http://www.mizar.org/language/syntax.html (February 10, 2005)
and syntax.txt (May 5, 2006).  Entropy process? :)

Why I am interested  in it:
  I have written a converter from syntax.txt to XML-file in order to get 
better understanding Mizar grammar.

> there is no automated (e.g. bison-like) connection between them and the
> Mizar parser.

I thougt about using Elkhound (GLR parsing) 
http://www.cs.berkeley.edu/~smcpeak/elkhound
or implementation GLR in OCaml
but for now my simple toy parser (in Ocaml) is coded by hand.

Michael Nedzelsky