[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Private DB
Hi,
On Tue, 26 Sep 2006, Freek Wiedijk wrote:
See mml.lar in the Mizar distro (hidden and tarski have to be
prepended).
Ah, thanks for pointing this out. (From now on I'll
painstakingly try to put all my directives in mml.lar order :-))
I don't think the benefit you may get from sticking to the order whenever
you increment the environment is worth the pain, but re-ordering from time
to time may be a good idea. It seems that a simple tool should be
distributed with the system to do that, or maybe even better, the Mizar
Emacs mode could be extended with such a feature. But anyway, the humble
'mml.lar' file is quite useful for various tasks ;-) The 'processing order
of articles', as we often call this list, now only vaguely reflects the
original process of article submissions. Many MML revisions (or
refactoring attempts) use this file to 'fix' certain steps of dependency
changes between articles by pushing and popping them within the list. That
was the case with separating the so called 'classical' and 'abstract'
parts of MML as proposed by Trybulec and Rudnicki in 2001 (articles that
use or not the notion of structures, i.e. depend or not on STRUCT_0),
which has been recently put into practice. A similar technique was also
used by Artur Kornilowicz to successively clarify the dependences of his
JORDAN article.
A few months ago I made an simple experiment sorting all notations in MML
according to 'mml.lar' and the result was quite promising in the sence
that there weren't many articles where the situation was not easily
'resolvable'. We started to analyse these cases, but then dropped the idea
for some more urging matters in hand. In the mean time, Artur Kornilowicz
used the ordering to optimize constructor lists in all articles. As you
raised the topic, I've run the same test on the current MML to see what it
looks like now. Apparently, there are more than a hundred files that pose
problems, but it seems that in most cases they can be fixed rather easily
by using a different redefinition for expansion.
for all the directives _but_ notations the order is irrelevant?
I am not sure about the "definitions" directive.
Ah yes, that's another one.
Indeed, this directive is also intentionally implemented to allow a kind
of "overloading" and so the order matters. The implementation of
registrations is probably also prone to lack of "robustness" when the
order is randomly mutilated, but the test proved that at least this
directive can painlessly be reordered according to 'mml.lar' in the
current MML.
A few people asked me to put the results somewhere they could see them
and help analyse the cases, so I've put them at
http://alioth.uwb.edu.pl/~adamn/result/
in folders 'notations' and 'definitions' together with a simple Perl
script I use to sort selected directives.
All the best,
Adam Naumowicz
======================================================================
Department of Applied Logic fax. +48 (85) 745-7662
Institute of Computer Science tel. +48 (85) 745-7559 (office)
University of Bialystok e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
======================================================================