Re: [mizar] Opinion to MML situation

[Adam Grabowski <adam@math.uwb.edu.pl>]

  Dear All,

On Wed, 26 Apr 2006, Piotr Rudnicki wrote:
> I would like to ask Adam Grabowski to give us some statistics before
> we start reviewing reviewing.  Could we know how many articles have been
>
> 	- submitted to MML?
> 	- accepted?
> 	- sent to the authors for upgrade?
> 	- rejected?
  all articles which were accepted later than January 1st, 2006
passed more careful review process than those accepted before
(for obvious technical reasons, some of these articles were sent before
this date).
  After four months, let me write some words about the review process.
All Mizar articles sent to the Library Committee of the Association
of Mizar Users have to pass some initial checkings. If the Mizar verifier
reports no errors wrt. the hottest version of the Mizar system available,
the submission is passed to three referees for review.
  The referee has two-three weeks for his work. Then review form
should be passed to the Library Committee.
  One of the basic elements of this form is the decision about the
inclusion of the article into the Mizar Mathematical Library.
As of now, there are five options available:

A. accept as is (editorial changes only, can be done by the editor)
B. accept, requires changes by the author to be approved by the editor
C. reject, substantial author's revisions needed before resubmission
   for another review
D. decision delayed, MML revision needed
E. reject, no hope of getting anything of value

  In 2006:
- in total, 26 articles were/are under review (submitted).
- 6 accepted (category A and B);
- 5 rejected (D, some C marks);
- 8 were sent back to authors (B and C grades);
- 7 are still under review.

  The articles with A marks are incorporated into the library as
soon as possible, suggested changes are done by the Library Committee.
  B and C grades need authors' feedback - it is their decision
of what to do with referees' suggestions of how to improve submission.
We experienced long life-cycle of some submissions (observe that C
grade imply another two-three weeks for review etc.).
  As it can be seen, hard to estimate acceptance factor. Also
hard to say who is really responsible for this slowdown of the
library growth pace.
  I agree with Professor Nakamura that articles which are sent to
the Library Committee for inclusion in the MML should be made public
immediately to avoid duplication of work. Of course, the formalization
in Mizar should be original. I can maintain webpage where abstracts
will be published immediately. I could also inform about new submissions
at mizar-forum (but as I remember, Artur Kornilowicz also proposed
to establish database of current formalization projects in Mizar, with
no feedback from the authors' side I know of, although Artur's idea was
to collect only drafts (promises?) of articles, not complete and correct 
Mizar sources).
  Personally, I do believe that if reviews will be taken into account
by authors, the quality of the Mizar Mathematical Library will be much 
higher. In this manner also 'good style of writing in Mizar' can be
worked out more effectively because before 2006 most of improvements were 
done by the Library Committee (but this activity is not excluded, even
in case of A-grade). That was very quick indeed but the authors repeated
their mistakes again and again. I think we can benefit this way
of thinking in the future.
  Regards,
  Adam Grabowski
  Library Committee of the Association of Mizar Users