[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] 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: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
======================================================================