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

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

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

The difference is in reconstructing the article in HTML. The syntax in 
comments allows users to do stupid things like:

theorem Foo
a+b =
::?SECTION Blah
b+a
proof ... end;

It is easy for the Mizar parser to disallow this stupidity. It is not easy 
for a lightweight parser which is not aware of the standard Mizar syntax.

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

If you by "Mizar verifier" also refer to the Mizar parser, then there is 
the above reason. The other passes (analyzer, checker) obviously will not 
deal with the metadata at all.

Josef