Re: [mizar] Formatter questions

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

On 5/12/10, Josef Urban <josef.urban@gmail.com> wrote:
> Hi Daniel,
>
> On 5/11/10, Daniel Matichuk <dmatichu@ualberta.ca> wrote:
>> I have a few questions about Mizar with regards to the formatter that I'm
>> working on:
>>
>> 1) Is there a comprehensive list of the meanings of all the intermediate
>> files that are generated for an article?
>
> Probably not.

For the xml-ized files, you can get some basic information by looking
up their top element at
http://mizar.uwb.edu.pl/version/current/doc/xml/Mizar.html, e.g.:
http://mizar.uwb.edu.pl/version/current/doc/xml/Mizar.html#Constructors

Josef

>
>> I have some vague ideas like "parx"
>> seems to be related to tokenization, but really I'd like a list of what
>> each
>> of these is for.
>
> .parx is a very new thing - an attempt to gradually xml-ize the
> Parser's output. It is a moving target and probably should not be
> relied upon in its current state.
>
>>
>> 2) Related to 1), is there an intermediate file that is an abstract
>> syntax
>> tree,
>
> To various degree the .par and .xml files.
>
> Best,
> Josef
>
>> or is it possible to have Mizar generate and abstract syntax tree for
>> an article? Ideally for formatting you'd just like an AST annotated with
>> identifiers.
>>
>> 3) Is the grammar posted at
>> http://mizar.uwb.edu.pl/version/current/doc/syntax.txt up-to-date?
>>
>