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

[trybulec <trybulec@math.uwb.edu.pl>]

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