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

Hi,

On Mon, 1 Dec 2008, Josef Urban wrote:

> On Sun, 30 Nov 2008, trybulec wrote:
>
>> Josef Urban wrote:
>> 
>>> 
>>> XML is easy to process by machines, and it is for this reason used as the 
>>> Mizar internal layer and input for other systems. Mizar parser produces 
>>> the XML from the Mizar human-like text, and I think it should stay this 
>>> way. That is: human-like keywords for humans, processed into 
>>> machine-understandable XML by Mizar parser.
>>> 
>>> The metadata info should certainly be optional during verification and 
>>> only required (if at all) when the article is submitted. I don't think 
>>> that broadening this discussion to other "pragmas" is going to help to fix 
>>> the problem Jesse asked about in a reasonable time. Inability to present 
>>> the metadata in HTML is a bug that should be fixed quickly, discussing new 
>>> Mizar features is useful but should be done separately and not in this 
>>> context .
>> 
>> 
>> As I wrote I have no opinion on the topic. I hoped that you would support 
>> XML :-)
>
> See above: using XML for direct human reading/writing is in my opinion quite 
> often abuse of a good technology developed for machines.

Yesterday I spoke to Grzegorz Bancerek (who I believe is another person 
'suspected' for supporting XML-style comments :-)) who tried to work out 
some sort of XML metadata standard within comments in his articles like 
YELLOW18, WAYBEL34 to be used by the FM presentation. But now Grzegorz is 
convinced that the XML part should be produced by the parser rather than 
by the users themselves, based on more user-friendly Mizar constructs.

>> On the other hand why not put the metadata into an unremovable comment, 
>> starting e.g. with
>> ::$
>
> That could be a first step, if we don't want to bother with enhancing the 
> Mizar parser. But if there is important information in such comments (title, 
> author, sections, nice names of theorems, important comments, etc.) that will 
> be used for presentation/searching/etc in HTML, FM, MML Query, etc., a parser 
> for these things is needed anyway, so why not re-use the Mizar parser? Also, 
> these things should appear in the XML form of the Mizar article, which is 
> currently produced by the Mizar parser.
>
>> More serious problem: what do you mean by 'Inability to present the 
>> metadata in HTML' ?
>
> Metadata like title, author, etc. are not present in the XML representation 
> of an article produced by the Mizar parser (because formally they are just 
> ignored comments).

That's another point that Grzegorz and I fully agree with. The more 
information about the article we can have within its source file, the 
better. Having the information split into several files like it is now 
(Mizar text, BIB-file metadata, FM translation patterns, maybe sth more) 
unnecessarily complicates all the presentation methods.

I believe the 'cluttering' of Mizar files as a result of putting a lot of 
data into the comments is in fact a problem only for those who work a lot 
on revising/improving the texts in the library, as they have to work on 
the 'raw' Mizar source. 'Normal' Mizar users, however, should rather (and 
I hope they do) use the presentation form for reading the articles - where 
it is possible to control the level of details in proofs, but also it 
would be very easy to suppress displaying various kinds of extra 
information put in the comments, were they not stripped away by the 
parser.

Regards,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================