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

Re: [mizar] Private DB

Hi Freek,
Come on. It looks horrible as demo goes. But look to an advaced article, e.g. JORDAN: the length of the article - about 6500 lines, the length of the Environment Declaration - about 50 lines. So we are talking about less than 1% of the text. I agree that for newbies it is disgusting. But in the case of advanced work creating the environment is nothing. And, as you observed you may copy the environment from a similar article. Working on a series of articles one copy and add new article several times. 
It is not that I believe nothing should be done. There are some serious 
problems with creating the environment but it is not the length of it.


Freek Wiedijk wrote:


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.


 


and run into troubles :-)


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.

 


Few teraflops would be better. Actually in the last year we have twice 
to drop the implemention of new features because of the combinatorial 
explosion.

Reagrds,
Andrzej