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

[trybulec <trybulec@math.uwb.edu.pl>]

Josef Urban wrote:

> On Sun, 14 Dec 2008, trybulec wrote:


> > Right. But I believe that the metadata probably will evolve 
> > independently and
>
>
> Independently from the Mizar parser? I think complete independence 
> (i.e., putting metadata into comments) is suboptimal (though certainly 
> better to have metadata in comments than not at all). For presenting 
> in HTML (and other systems), it would be good if metadata were present 
> in the XML form of article produced by the Mizar parser. That means 
> the parser should be aware of them, at least to some minimal extent 
> (e.g., recognize the start and end bracket of metadata, and treat 
> everything in between as a string, and output this in a proper place 
> in the XML).


Actually, I would rather have a cross reference to the metada in a comment.

Like

::?  SECTION  ABC

and at ABC are the metadata related to the section.

I accept that you want the metadata be presented in XML, why they should 
be produced by the Mizar parser?
What is the difference to you how you get them?

> One standard is the Dublin Core (DC), my Perl hack currently produces 
> proper DC XML elements from the starting comments in .miz files. There 
> is no reason why the Mizar parser could not do it too from whatever 
> human-friendly syntax.
There is no reason for the Mizar verifier to bother with metadata.

Regards,
Andrzej