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

Dear Jesse,

In Algol 60 a comment was a part of the language. The syntax was
     comment   TEXT ;

where TEXT was an arbitrary string of characters ( the semicolon itself
was not allowed)
We treat now comments as something that actually is not a part of the
language. I would rather
have "pure Mizar" with only these informations that are necessary for
the verifier.
We have now some features that should not be in pure Mizar and probably
should be replaced by pragmas:
they may be classified in the following categories:
i. temporary pragmas:   '@proof'  - to suspend verification
ii. library pragmas:   'canceled' - to keep numeration correct
iii. editorial pragmas:  repeated 'begin' - to divide article into section.
iv. maybe some others

We tried - on our seminar - to find common solution, but the categories
are so different that probably
there is none.

Recently, after reading your letter, we discussed the problem again with
Czeslaw and it seems that for the metadata the proper solution is to
have an XML-envelope of the Mizar article. Maybe something like
      <DOCUMENT>
         "the place for metadata"
      <ARTICLE>
          "the Mizar article"
      </ARTICLE>
      </DOCUMENT>
(mind you, I know almost nothing on XML, so it might quite naive).

Then from such XML document we may extract the Mizar article and process
it in the usual way.
"the Mizar article" is probably not the exact citation: we have '<' as a
symbol in Mizar. Still extracting the Mizar article should not be too
complicated. Maybe we can be more precise and have the form

      <DOCUMENT>
         "the place for metadata"
      <ARTICLE>
      <ENVIRONMENT DECLARATION>
          "directives"
      </ENVIRONMENT DECLARATION>
       <TEXT PROPER>
          "the text proper"
      </TEXT PROPER>
      </ARTICLE>
      </DOCUMENT>

Then, 'environ' and 'begin' (if necessary) may be added while extracting
the Mizar article.  The directives and the text proper are written in
two different languages, anyway.

      <DOCUMENT>
         "the place for metadata"
      <ARTICLE>
      <ENVIRONMENT DECLARATION>
          "directives"
      </ENVIRONMENT DECLARATION>
       <TEXT PROPER>
        <SECTION>
          "the text proper"
        </SECTION>
          ...
        <SECTION>
          "the text proper"
        </SECTION>
      </TEXT PROPER>
      </ARTICLE>
      </DOCUMENT>

Then we may put in the <SECTION> the title and maybe even the summary of
the section. And the grammar of Mizar will be a little bit simpler: no
repetition of 'begin'.

Regards,
Andrzej

Jesse Alama wrote: