« Return to Thread: an extension of the mizar language for dealing with article metadata

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

by Josef Urban :: Rate this Message:

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 .

Josef

On Fri, 28 Nov 2008, trybulec wrote:

> Josef Urban wrote:
>
>>
>> Hi,
>>
>> I think the new directives should not use XML syntax, simply because it
>> is ugly, verbose, and unnecessary. I don't think XML should be used for
>> direct human authoring and reading, just as assembly language should
>> not. The new directives should be normal Mizar keywords like "author",
>> "title", etc.
>>
> Hi:
>
> It is not exactly to the point but we talk about 'reserved words' not
> 'keywords'. A keyword is a word that characterize
> the semantics of the article like 'compact', 'homology group' and so on.
> So, in Mizar - the symbols. Not all of them.
> 'Function' is hardly a keyword - too often used. The tradition of the
> misuse of the word goes back to Algol 60, the Authors of the declaration
> did not know what 'keyword' means.
>
> Some of my colleagues tried to convince me that we should use XML because
> of ready tools like browsers that present the text in human readable form.
> It is true?
>
> The Mizar system, at least for me, is first a Math Assistant. When I work
> on an article (it happens) I am not interested in the authors' name and I
> have yet to invent the title. I would like to keep the Mizar syntax, in
> this role, as simple as possible.
> I do not see why the pragmas should be part of the language. The only
> their 'operational semantics' is to ignore them.
>
> We discuss only the library pragmas. What about temporary pragmas, used to
> suspend the processing. We need
> more of them. Piotr Rudnicki, if I recall, argued for '@now' or '@by' to
> suspend the checker . '@proof' does not help,
> if we have large Diffuse Statement. In old Mizar (on Cyber 72} we have
> pragma 'virtual EOF' , useful because sometimes ANALYZER take more time
> that the CHECKER.
> So what about them, again new 'reserved' words?
>
> What about library pragmas? Again we need more, not only 'canceled',
> missing for schemes anyway. E.g. 'obsolete' for theorems or schemes that
> are later proved in a stronger form, and original ones should not be used.
> For instance
> FUNCT_1:sch 2
> that it is still used, even if
> CLASSES1:sch 1
> should be used instead.
>
> So we need, for different purposes various systems of pragmas that may be
> developed separately and do not think they should be mixed with Mizar.
>
> Regards,
> Andrzej
>
>
>
>
>

« Return to Thread: an extension of the mizar language for dealing with article metadata