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

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

Hi,

On Wed, 3 Dec 2008, Adam Naumowicz 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.

I think what Grzegorz did was at least some solution for improving 
presentation and including metadata, and it is certainly much better than 
doing nothing.

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

This is (finally!) in this discussion one good real point against too much 
documentation and having whole Isar-style papers mixing TeX and formal 
text: Mizar articles form a library that is sometimes refactored, and 
theorems and definitions can be moved to other places and articles. 
Refactoring the corresponding natural language is additional effort that 
in some (very rare) cases could equal to re-writing a large part of a 
published paper :-).

But I don't think this reasoning should be used to forbid interested 
people to put more value into the Mizar formalizations. MML is a mess 
anyway, and so far nobody said "let's stop writing articles, we cannot 
maintain the library already". Some amount of chaos is natural, and we 
should rather think about ways and tools for letting more people improve 
MML, which is certainly some wiki-like functionality. Fixing obvious bugs 
and inaccuracies in natural language is easy, and if there are people 
interested in reading the articles, they will do the job (at least in 
Wikipedia they very often do).

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

I think that if "stripping presentation" is needed at all (and I doubt it: 
nobody strips comments now before doing revisions - I think even contrary 
might be closer to truth: comments often provide useful clues), having a 
tool for it is easy.

Josef