Re: [mizar] an extension of the mizar language for dealing with article metadata

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Fri, 28 Nov 2008, trybulec wrote:

> Josef Urban wrote:
>
> > This is written in Jesse's e-mail: the metadata could be processed by 
> > standard Mizar-based tools that are currently used for creating the HTML 
> > representation, are (going to be) used for collecting data for MML 
> > Query, and possibly also other things like FM and MPTP. It is not 
> > practical to keep these data separately and process them by separate 
> > tools, especially when they are quite a natural part of the articles.
> 'natural' ?
>
> Well, if you mean by an 'article' a mathematical paper you're right, if it 
> is thought as a script for the verifier, you're not.

So why is the keyword "begin" allowed multiple times to introduce 
sections, and why do all articles start with the standard header 
containing author and title, why are comments allowed at all? If there 
is no need to process and present these article parts in HTML, MML Query, 
FM, MPTP, etc., I suggest to disallow these "unnatural" parts also in the 
article (.miz) files. Or perhaps they are useful, and we should properly 
care about them? Writing fragile Perl hacks that will hardly be usable on 
Windoze is then hardly the right way: the Mizar parser should do this.

Josef

> Regards,
> Andrzej