Re: an extension of the mizar language for dealing with article metadata
Josef Urban <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
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 >