[mizar] Re: calculating the transitive closure of required mizar items for a theorem

[Jesse Alama <alama@stanford.edu>]

Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:

> On Wed, 7 Nov 2007, Josef Urban wrote:
>
>>> Option (1) may also work.  I would create one enormous MIZAR file
>>> containing everything from the union of the articles metioned in the
>>> environment of the article in which I prove x, and then write some code
>>> to whittle away at the huge file until the removal of anything causes an
>>> error which implies that the proof x is incorrect.
>>
>> Yes, there might even be similar utilities for "cleaning the
>> environment" in the Mizar CVS. One danger of your approach (having
>> all inside the article) is that some (possibly redundant)
>> registrations will be needed for parsing other (possibly redundant)
>> registrations, causing irrelevant errors.
>
> One simple idea for doing this practically is to experiment with the
> Article.ecl file. This file contains all registrations imported from
> the article's environment, and removal of registrations from it should
> be OK (it will not cause parse errors to other items in it, because
> they are already parsed (in the XML form)).

I tried looking at the .ecl file, and I find it to be totally cryptic.
What does

    <RCluster>
    <ArgTypes/>
    <Typ kind="M" nr="1">
      <Cluster/>
    </Typ>
    <Cluster>
      <Adjective nr="1"/>
      <Adjective nr="2"/>
    </Cluster>
  </RCluster>

mean (for example)?  I assume this corresponds to some mizar item in
some article.  Can I compute that information from the XML?

> So assuming that your Article contains only theorems, the method for
> determining environmental registrations needed for ThX is to:
> - delete all but ThX from Article
> - accommodate
> - check that Article is without verification errors (it should at this
> point)
> - try deleting one XML entry (RCluster,FCluster,CCluster) from
> Article.ecl at a time, followed by verification; if error occurs, keep
> the entry, otherwise get rid of it

This sounds practical, but it would be nice to know, when I delete
something from the .ecl file, what mizar item I just deleted.  In the
example above, for instance, I don't know what mizar item in what
article I would be deleting if I were to simply delete it from the .ecl
article.  Ideally I would have a procedure for finding an item that
doesn't have to do with my theorem and deleting its text a local copy of
the MML, thereby "trimming" the MML until no more trimming can be done.

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)