[Date Prev][Date Next] [Chronological] [Thread] [Top]

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


Hi Jesse,

On Fri, 14 Dec 2007, Jesse Alama wrote:


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)?
ftp://mizar.uwb.edu.pl/pub/version/doc/xml/Mizar.html#RCluster . The documentation could be improved (it is directly in the Mizar sources though, to keep it reasonably in sync with the datastructures). Also, I could add the DTD specs (e.g. in the .rng format: ftp://mizar.uwb.edu.pl/pub/version/doc/xml/registrations.rng) to the .ecl file header, as is common in the xml world. (I am however not sure if these URLs are the canonical place for these docs). 



I assume this corresponds to some mizar item in
some article.  Can I compute that information from the XML?
I am a bit surprised that there is not more info in .ecl :-). For the .dfs (definitional expansions), there is more info, e.g. 

<Definiens constrkind="R" constrnr="1" aid="XBOOLE_0" defnr="10" relnr="52">
says that this definiens corresponds to the 10-th definitional theorem in XBOOLE_0 (i.e. to XBOOLE_0:def 10). It should be easy to fix the .ecl file similarly (so that e.g. the RCluster elemnt would carry similar info there), and I don't know an easy alternative to it. 


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.
Right, you need the additionally info for this. I though it was already there. 

Josef