Re: [mizar] Private DB

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Josef,

>If someone new does the mistake of trying to understand the
>black magic behind environmental directives, he is probably
>lost as a Mizar author forever.  The old directives could
>remain for fine-tuning if needed.

I totally agree with Josef.  The ICMS demo
<http://www.cs.ru.nl/~freek/demos/> _very_ clearly showed how
inferior Mizar was in this respect.  Look at the "environment"
parts of the various formalizations:

  Isabelle:
    "imports Complex"

  HOL Light:
    "needs "Multivariate/misc.ml;;"

  ProofPower:
    "open_theory "analysis";"

  Coq:
    "Require Imports Reals.
     Require Imports Fourier."

  Mizar:
    "vocabularies ARYTM, ARYTM_1, RELAT_1, ARYTM_3, FUNCT_1, ABSVALUE, SEQ_4,
      SEQ_2;
     notations SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1, COMPLEX1, FUNCT_1,
       RELSET_1, FUNCT_2, SEQ_4, XXREAL_0, PARTFUN3;
     constructors PARTFUN1, XXREAL_0, REAL_1, COMPLEX1, PARTFUN3;
     registrations RELSET_1, XREAL_0, MEMBERED, SEQ_1, RELAT_1, FUNCT_2;
     requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
     definitions SEQ_4;
     theorems XREAL_1, COMPLEX1, SEQ_1, SEQ_4, FUNCT_1, FUNCT_2, XCMPLX_1,
       ABSVALUE;"

See my point?  Also, fighting with the environment is one of
the things that I really hate most in writing a Mizar article.
Which is a pity, as the notations and clusters and so on, they
are wonderful.  But you should be able to get them by just
saying "give me all!" and go from there.

Really, computers are not 640K PC's anymore that run at a few
MHz.  They can handle a lot of stuff at once, believe me.

Freek