an extension of the mizar language for dealing with article metadata

[Josef Urban]

Hi Freek,

On Mon, 5 Jan 2009, Freek Wiedijk wrote:

> Hi Josef,
>
> A happy new year!

Happy New Year!
(But I really wonder if such greetings belong to globalised fora: e.g.
Jews consider Christmas a pagan ritual :-)

>> How about removing the "vocabularies" directive
>> completely? The "notations" would say to the parser which
>> symbols are available.
>
> To me this seems a much more drastic change than what I
> was proposing.  I guess it also would mean unifying the
> vocabulary and article name spaces?

I think there would be no "vocabulary".

Josef

[Freek Wiedijk]

Hi Josef,

>>To me this seems a much more drastic change than what I
>>was proposing.  I guess it also would mean unifying the
>>vocabulary and article name spaces?
>
>I think there would be no "vocabulary".

So all vocabularies would be always active?  But then I
could break existing articles by introducing new symbols
in my vocabulary to MML.  So how should I test for that?

Or would you want to introduce the vocabulary elements
together with the notation, always?  So that sounds a more
radical change than what I proposed.  (My proposal was
just to move text from one file to another, but without
the system really changing.)

Freek

[Josef Urban]

On Mon, 5 Jan 2009, Freek Wiedijk wrote:

> Hi Josef,
>
>>> To me this seems a much more drastic change than what I
>>> was proposing.  I guess it also would mean unifying the
>>> vocabulary and article name spaces?
>>
>> I think there would be no "vocabulary".
>
> So all vocabularies would be always active?

no, symbols (which need to be known beforehand by the existing Mizar
parser) would be taken from
- notations (which sort of contain them already now)
- definitions inside the article (which might need some syntax change to
allow easy parse of the new symbols)

> Or would you want to introduce the vocabulary elements
> together with the notation, always?

yes

> So that sounds a more
> radical change than what I proposed.  (My proposal was
> just to move text from one file to another, but without
> the system really changing.)

yes; I think something really should be done with the environment "black
magic"; perhaps even the "constructors" directive could be made only
optional or removed totally; if this causes more notation clashes, then
they should be resolved by renaming the overloaded symbols, not by
resorting to black magic operations with the environment header

Josef

[Freek Wiedijk]

Hi Josef,

>yes; I think something really should be done with the
>environment "black magic";

I agree.  I also think that given the current Mizar culture,
it just won't happen.

If even my very modest proposal to integrate the vocabulary
files into the articles is seen as a huge problem for
maintaining the MML (it isn't!) even bigger changes do not
stand any chance of happening.  I fear.

>perhaps even the "constructors" directive could be made only
>optional or removed totally;

I especially am always very surprised by the "theorems"
directive.  Certainly it only needs an utterly trivial pass
over the article to find out what should go in there.

I often need to run Mizar twice because I forgot to add an
article to the theorem directive.  That is a serious pain
in the you-know-where.

Freek

[Piotr Rudnicki]

On Mon, Jan 05, 2009 at 07:48:58PM +0100, Freek Wiedijk wrote:

> I especially am always very surprised by the "theorems"
> directive.  Certainly it only needs an utterly trivial pass
> over the article to find out what should go in there.
>
> I often need to run Mizar twice because I forgot to add an
> article to the theorem directive. ...

I support Freek.  Is the extra pass even needed?  Can the import
of theorems be done on the fly?

On the other hand, it is interesting what was the past motivation for
introducing the theorems directive.  (With the schemes directive the
story is different).

Best,

--
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr

[trybulec]

Piotr Rudnicki wrote:

<>On Mon, Jan 05, 2009 at 07:48:58PM +0100, Freek Wiedijk wrote:

I support Freek. Is the extra pass even needed? Can the import
of theorems be done on the fly?

On the other hand, it is interesting what was the past motivation for
introducing the theorems directive. (With the schemes directive the
story is different).

< />

You should remember. A mispelling of a reference to a theorem more often happens than
the need of adding  the name of theorems file to the 'theorems' directive.

Maybe more important is that you should first run PARSER (for the Text Proper), to generate
a file for the ACCOMMODATOR (maybe incorrect) and then to run the VERIFIER. Clumsy.

Regards,
Andrzej

[Grzegorz Bancerek]

Hi,

Happy New Year

Quoting Josef Urban <urban@...>:

> The FM translation technology should rather use notation (pattern)
> for mapping to TeX than the symbol level, because one Mizar symbol
> can have very different contexts of use, and possibly very different
> TeX notations (I think we already talked about this one with Grzegorz
> some time ago).

In FM translation the only almost but not quite unlike stable resource
is used:
formats (symbol+arity). For example, plus in expressions x+y, x+, +x etc.
may have different presentation in LaTeX. Namely, the first and third
pluses are
represented just by + but the second by ^+
Of course, there are bigger differences in translation for other symbols.

Patterns uses types of arguments annotated with constructors which change from
version to version of distribution. Maintenance of translation patterns
based on
such resource may be quite interesting.

Best,
Grzegorz

[Josef Urban]

On Tue, 6 Jan 2009, Grzegorz Bancerek wrote:

>> The FM translation technology should rather use notation (pattern) for
>> mapping to TeX than the symbol level, because one Mizar symbol can have
>> very different contexts of use, and possibly very different TeX notations
>> (I think we already talked about this one with Grzegorz some time ago).
>
> In FM translation the only almost but not quite unlike stable resource is
> used:
> formats (symbol+arity). For example, plus in expressions x+y, x+, +x etc.
> may have different presentation in LaTeX. Namely, the first and third pluses
> are
> represented just by + but the second by ^+
> Of course, there are bigger differences in translation for other symbols.
>
> Patterns uses types of arguments annotated with constructors which change
> from
> version to version of distribution. Maintenance of translation patterns based
> on
> such resource may be quite interesting.

I think there is one simple option: keep the TeX symbol in the article
with the definition if needed. There could still be the current table on
the format level used as a default (e.g. x+y will most often be x+y in
TeX), and the info from patterns would override the format default (if
there is any).

My knowledge of the current FM translation technology is limited, but I
think this could take care of the maintenance problem and also allow the
users to easily provide new TeX presentation info directly in the article
(without learning about FM formats).

Josef

[Josef Urban]

On Tue, 6 Jan 2009, trybulec wrote:

> Piotr Rudnicki wrote:
>
>> <>On Mon, Jan 05, 2009 at 07:48:58PM +0100, Freek Wiedijk wrote:
>>
>> I support Freek. Is the extra pass even needed? Can the import
>> of theorems be done on the fly?
>>
>> On the other hand, it is interesting what was the past motivation for
>> introducing the theorems directive. (With the schemes directive the
>> story is different).
>>
> You should remember. A mispelling of a reference to a theorem more often
> happens than
> the need of adding  the name of theorems file to the 'theorems' directive.

Side note: If you use Emacs, use Alt-/ for dynamic completion of such
identifiers. For example, if you want to write "SQUARE_1", and have
"SQUARE_1" already in the environment, then only type "SQ" or "SQU" and
then press ALT-/ to complete. If there is no dynamic completion, something
is wrong (you mistyped or the identifier is nowhere in the article yet).

One possible additional check (in Emacs) would be to watch if the added
identifiers are in mml.lar or the current environment after entering
"by.*;" . Probably not a big deal.

Provided that (using such mechanisms) you will never mistype here, Freek's
complaint wins (I think his problem is fairly frequent too). But Freek's
complaint can be also dealt with automagically in Emacs :-) (i.e. the
environment directive appended).

> Maybe more important is that you should first run PARSER (for the Text
> Proper), to generate
> a file for the ACCOMMODATOR (maybe incorrect) and then to run the VERIFIER.
> Clumsy.

Just one more pass in a multipass compiler :-). If white char is strictly
required before and after "by" and "from" (I am not sure now), then a very
cheap pass. But I would do a check against mml.lar (plus local db) before
running accommodator, and complain if there is a typo instead of
accommodating.

Josef

[Freek Wiedijk]

Dear Andrzej,

>Maybe more important is that you should first run PARSER
>(for the Text Proper), to generate a file for the
>ACCOMMODATOR (maybe incorrect) and then to run the
>VERIFIER. Clumsy.

Of course you could also have a _separate_ tool that would
find all theorems used by your article, and then update the
article if necessary, by adding missing references to the
theorems directive.

You could then add that to mizf at the start.  So mizf then
would be:

(1) run that tool
(2) continue with the current mizf

If the article was changed because the theorems directive was
extended by the tool, accomodator would be run by the second
step (so yes, then you parse the article before _and_ after
accomodator), but that's unavoidable.  If you had updated the
theorems directive yourself, accomodator would be run too.

Maybe it's in some sense clumsy to do it like this, but
getting irritated now and again (in my case: quite often) by
having to change the theorems directive when in the middle
of working on my formalization is clumsy too.  (I have to
go to the environment, change stuff there, reflow the lines
if necessary to get under the 80 column limit, and then
somehow get back to where I was working.  It's distracting.
And, as I said, often I forget about the theorems directive,
and get irritated by the error message as well.)

So having a tool that messes with your article (if only with
the environment) sounds a bit scary, but error messages
are inserted in the article as well, so it's not a very
big change.

Freek

[trybulec]

Josef Urban wrote:

>
>
> On Tue, 6 Jan 2009, trybulec wrote:
>
>

> Side note: If you use Emacs, use Alt-/ for dynamic completion of such
> identifiers. For example, if you want to write "SQUARE_1", and have
> "SQUARE_1" already in the environment, then only type "SQ" or "SQU"
> and then press ALT-/ to complete. If there is no dynamic completion,
> something is wrong (you mistyped or the identifier is nowhere in the
> article yet).
>
> One possible additional check (in Emacs) would be to watch if the
> added identifiers are in mml.lar or the current environment after
> entering "by.*;" . Probably not a big deal.
>

Better to check DB for the #.THE file. I quite often work will partial
DB, so checking MML.LAR does nor help.

> Provided that (using such mechanisms) you will never mistype here,
> Freek's complaint wins (I think his problem is fairly frequent too).
> But Freek's complaint can be also dealt with automagically in Emacs
> :-) (i.e. the environment directive appended).
>
Thanks for the explanation. I should get more accustomed with the Mizar
mode in emacs. I believe it is a proper way
to deal with the preprocessing.

>> Maybe more important is that you should first run PARSER (for the
>> Text Proper), to generate
>> a file for the ACCOMMODATOR (maybe incorrect) and then to run the
>> VERIFIER. Clumsy.
>
>
> Just one more pass in a multipass compiler :-). If white char is
> strictly required before and after "by" and "from" (I am not sure
> now), then a very cheap pass. But I would do a check against mml.lar
> (plus local db) before running accommodator, and complain if there is
> a typo instead of accommodating.

No so cheap. One cannot use a standard PARSER (lexical analysis
impossible), so we need a special version of
PARSER and moreover a special version of SCANNER (TOKENIZER). One bloody
program more to maintain.

The "division of labor " is now clear. The ACCOMMODATOR processes the
Environment Declaration and
creates the environment of the article, an ad hoc little theory, sort of.

Then the VERIFIER (RELPREM, EXPORTER, whatever) process the article in
the given environment. I would not
change it.

I am not against interactive help with creating the Environment
Declaration. I am definitely pro.It is much needed But it should not be
mixed with other utilities.

Regards,
Andrzej

[trybulec]

Freek Wiedijk wrote:

>Of course you could also have a _separate_ tool that would
>find all theorems used by your article, and then update the
>article if necessary, by adding missing references to the
>theorems directive.
>
>  
>
OK with me. You have to write new SCANNER.  If SCANNER would pass the
token as the file name,
then action for PARSER is clear: take the spelling and write in on a
file or somewhere.

>You could then add that to mizf at the start.  So mizf then
>would be:
>
>(1) run that tool
>(2) continue with the current mizf
>
>  
>
Better change the name. I would like to use old mizf

>Maybe it's in some sense clumsy to do it like this, but
>getting irritated now and again (in my case: quite often) by
>having to change the theorems directive when in the middle
>of working on my formalization is clumsy too.  (I have to
>go to the environment, change stuff there, reflow the lines
>if necessary to get under the 80 column limit, and then
>somehow get back to where I was working.  It's distracting.
>And, as I said, often I forget about the theorems directive,
>and get irritated by the error message as well.)
>
>  
>

I rather welcome an opportunity to rest, to do a routine job. Maybe I am
too lazy.

>So having a tool that messes with your article (if only with
>the environment) sounds a bit scary, but error messages
>are inserted in the article as well, so it's not a very
>big change.
>
>  
>
Error messages are comments, they are pruned anyway.

Regards,
Andrzej

[Josef Urban]

On Wed, 7 Jan 2009, trybulec wrote:

> Freek Wiedijk wrote:
>
>> Of course you could also have a _separate_ tool that would
>> find all theorems used by your article, and then update the
>> article if necessary, by adding missing references to the
>> theorems directive.
>>
>>
> OK with me. You have to write new SCANNER.  If SCANNER would pass the token
> as the file name,
> then action for PARSER is clear: take the spelling and write in on a file or
> somewhere.

something like:
perl -e 'local $/;$_=<>; s/::.*//g; while(m/\sby\s([^;]*);/g) {@a=$1=~m/[\s,](\w*)\s*:/g; @h{@a}=()} print join(",", sort keys %h),"\n"' foo.miz

>> So having a tool that messes with your article (if only with
>> the environment) sounds a bit scary, but error messages
>> are inserted in the article as well, so it's not a very
>> big change.
>>
>>
> Error messages are comments, they are pruned anyway.

Automated creation of skeletons in Emacs messes the article a lot (making
some people quite happy). It silently uses a modified Mizar parser
(lisppars) for parsing the article into Lisp-friendly notation. An
additional "pass" that nobody knows about :-). But I think the above Perl
hack does the job in this case.

Josef

[Adam Naumowicz]

Hi Josef,

On Wed, 7 Jan 2009, Josef Urban wrote:

> On Wed, 7 Jan 2009, trybulec wrote:
>
>> Freek Wiedijk wrote:
>>
>>> Of course you could also have a _separate_ tool that would
>>> find all theorems used by your article, and then update the
>>> article if necessary, by adding missing references to the
>>> theorems directive.
>>>
>>>
>> OK with me. You have to write new SCANNER.  If SCANNER would pass the token
>> as the file name,
>> then action for PARSER is clear: take the spelling and write in on a file
>> or somewhere.
>
> something like:
> perl -e 'local $/;$_=<>; s/::.*//g; while(m/\sby\s([^;]*);/g)
> {@a=$1=~m/[\s,](\w*)\s*:/g; @h{@a}=()} print join(",", sort keys %h),"\n"'
> foo.miz

I like your 'constructive' argument in the discussion very much :-)
Indeed, it seems to work fast enough to simply put it in the user
interface (either the mizf script or Emacs mode) as an independent pass
and not complicate the parser at all. But I noticed that your hack, as it
stands now, won't work well with iterative equalities (no semicolon after
some by's), if a reference starts the justification of the first iteration
step (no extra space or comma) and also if terms like the Cartesian
product ([:X,Y:]) occur in the equalities. Still, a slightly modified
version passed a few tests I could think of right now:

perl -e 'local $/;$_=<>; s/::.*//g; while(m/\sby\s([^;.]*)(;|\.)/g)
{@a=$1=~m/,?(\w*)\s*:/g; @h{@a}=()}
print join(",", sort keys %h),"\n"' foo.miz

Best,

Adam

======================================================================
Department of Applied Logic            fax. [phone]
Institute of Computer Science          tel. [phone] (office)
University of Bialystok                e-mail: adamn@...
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================

[Josef Urban]

On Wed, 7 Jan 2009, Adam Naumowicz wrote:

> Hi Josef,
>
> On Wed, 7 Jan 2009, Josef Urban wrote:
>
>> On Wed, 7 Jan 2009, trybulec wrote:
>>
>>> Freek Wiedijk wrote:
>>>
>>>> Of course you could also have a _separate_ tool that would
>>>> find all theorems used by your article, and then update the
>>>> article if necessary, by adding missing references to the
>>>> theorems directive.
>>>>
>>>>
>>> OK with me. You have to write new SCANNER.  If SCANNER would pass the
>>> token as the file name,
>>> then action for PARSER is clear: take the spelling and write in on a file
>>> or somewhere.
>>
>> something like:
>> perl -e 'local $/;$_=<>; s/::.*//g; while(m/\sby\s([^;]*);/g)
>> {@a=$1=~m/[\s,](\w*)\s*:/g; @h{@a}=()} print join(",", sort keys %h),"\n"'
>> foo.miz
>
> I like your 'constructive' argument in the discussion very much :-) Indeed,
> it seems to work fast enough to simply put it in the user interface (either
> the mizf script or Emacs mode) as an independent pass and not complicate the
> parser at all.

which will (rightfully) make Windoze users suffer for their choice of
(non)operating system (why would a mere "user" need a thing like Perl
shipped with OS?? (give him Ms. Word with Mr. Clippy instead! :-))

the usual solution (if we care about them) is to rewrite it in Emacs Lisp,
or really use Pascal and ship another binary; or just tell them to install
Perl if they care, or to use a real OS

> But I noticed that your hack, as it stands now, won't work
> well with iterative equalities (no semicolon after some by's),

yes, I also ignored "from" which is probably easy

> if a reference
> starts the justification of the first iteration step (no extra space or
> comma) and also if terms like the Cartesian product ([:X,Y:]) occur in the
> equalities. Still, a slightly modified version passed a few tests I could
> think of right now:
>
> perl -e 'local $/;$_=<>; s/::.*//g; while(m/\sby\s([^;.]*)(;|\.)/g)
> {@a=$1=~m/,?(\w*)\s*:/g; @h{@a}=()}
> print join(",", sort keys %h),"\n"' foo.miz

looks OK to me

Josef