Re: [mizar] Formatter questions

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

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.

> 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?
>