Re: [mizar] Re: Mizar Parser

[Grzegorz Bancerek <bancerek@cs.shinshu-u.ac.jp>]

Freek:

Freek Wiedijk wrote:
> 
> Grzegorz:
> 
> >MML Query can be downloaded. It is a bunch of perl scripts
> >plus 1Gb of data.
> 
> 1Gb!  That's a lot!  Why is it so big?  I'd hate to have to
> download that for each new version of MML!

This is experimental version and I didn't care of memory.
After gzip it is only %6 (60kb).
You don't have to download each version of MML. You may download
programs which generate this data. If new version of MML is only
submittion of new article it will be quite fast in update.
But revision causes regeneration and it takes about 12 hours
on 1GHz under linux.  Download is faster.

> >The names of items can be found in  Mizar eXtended Abstracts
> >  http://megrez.mizar.org/pub/mxa/
> 
> Are those mxa's available in just one tar.gz file?  And is
> there a set of ".mxa.html" files that contain hyperlinks,
> like the jfmabstr.tar.gz?
> 
> >Now, there is no usable description of MML Query system.
> 
> Is there a list of example queries?  I think that's all you
> need to understand how to use it?

I am preparing such list. Now you may read small description
with some examples:
  http://megrez.mizar.org/mmlquery/description.html

Sorry for the mess.

> >You can get there full info of a statement in any place of
> >mizar article.
> 
> I don't understand this.  Suppose I'm in emacs in an article
> I'm writing, I'm in some formula (say "f.(-x) = -f.x"), and
> want to know the constructors of that formula (because I want
> to know the constructor of the "-").  Now what do I do?

In lastest versions of mizarmode (see "mizar.el" in Mizar disrtibution)
in Mizar menu|Constr. Explanation | Verbosity  mark constructors list.
After Run Mizar you will have places (near "by" or ";") to click.
It is better to mark also 
  Mizar menu|Constr. Explanation | Underline explanation points
Then you may click them shift+mouse-2 and in other window you
will get a list or a formula with mml query constructor names.
Now mouse-2 - go to abstract , mouse-1-2 - go to mml query.

Grzegorz