Re: Size of Mizar/MML
Adam Naumowicz adamn _AT_ math.uwb.edu.pl <[email protected]> Thu, 05 Jun 2025 22:01:51 +0200
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
------O13XHIHZ65RG97RT6TUU0WJM0LJN5C Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=UTF-8 Hi, Have a look at the statistics of the newest MML provided by the MMLQue= ry (http://mmlquery=2Emizar=2Eorg)=2E =E2=81=A3Cheers, Adam W dniu 5 cze = 2025, 17:52, o 17:52, u=C5=BCytkownik "Fabian Huch huch _AT_ in=2Etum=2Ede= " <owner-mizar-forum@mizar=2Euwb=2Eedu=2Epl> napisa=C5=82: >Dear Mizar Com= munity, > >I am currently creating a comparison of large libraries of ITPs= =2E I am >only considering libraries with more than 1M (nonempty) LOC, of = which I > >know (in alphabetical order): ACL2, HOL4, Isabelle, Lean, Metama= th, >Mizar, PVS, Rocq=2E >To that end, I want to approximate the number of= definitions (incl=2E >axioms / excl=2E abbreviations, instances, fixed va= lues/constants, >examples) and proven proper theorems (excl=2E automatical= ly generated >ones) by simple analysis of the sources, without running the= system=2E > >For Mizar/MML, my approach would be to look at tokens in =2Em= iz files and > >count: > >For definitions: "definition" > >For theorems: "t= heorem" and "scheme" > > >Does this sound reasonable? I am missing somethin= g? Any hints are >appreciated=2E > > >Best, > >Fabian Huch ------O13XHIHZ65RG97RT6TUU0WJM0LJN5C Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable <html><head></head><body style=3D"zoom: 0%;"><div dir=3D"auto">Hi,<br><br><= /div> <div dir=3D"auto">Have a look at the statistics of the newest MML pro= vided by the MMLQuery (<a href=3D"http://mmlquery=2Emizar=2Eorg">http://mml= query=2Emizar=2Eorg</a>)=2E<br><br></div> <div dir=3D"auto"><!-- tmjah_g_12= 99s -->Cheers,<!-- tmjah_g_1299e --><br></div> <div dir=3D"auto"><!-- tmjah= _g_1299s -->Adam<!-- tmjah_g_1299e --></div> <div class=3D"gmail_quote" >W = dniu 5 cze 2025, o 17:52, u=C5=BCytkownik "Fabian Huch huch _AT_ <a href= =3D"http://in=2Etum=2Ede">in=2Etum=2Ede</a>" <<a href=3D"mailto:owner-mi= zar-forum@mizar=2Euwb=2Eedu=2Epl" target=3D"_blank">owner-mizar-forum@mizar= =2Euwb=2Eedu=2Epl</a>> napisa=C5=82: <blockquote class=3D"gmail_quote" = style=3D"margin: 0pt 0pt 0pt 0=2E8ex; border-left: 1px solid rgb(204, 204, = 204); padding-left: 1ex;"> <pre class=3D"blue">Dear Mizar Community,<br><br= >I am currently creating a comparison of large libraries of ITPs=2E I am <b= r>only considering libraries with more than 1M (nonempty) LOC, of which I <= br>know (in alphabetical order): ACL2, HOL4, Isabelle, Lean, Metamath, <br>= Mizar, PVS, Rocq=2E<br>To that end, I want to approximate the number of def= initions (incl=2E <br>axioms / excl=2E abbreviations, instances, fixed valu= es/constants, <br>examples) and proven proper theorems (excl=2E automatical= ly generated <br>ones) by simple analysis of the sources, without running t= he system=2E<br><br>For Mizar/MML, my approach would be to look at tokens i= n =2Emiz files and <br>count:<br><br>For definitions: "definition"<br><br>F= or theorems: "theorem" and "scheme"<br><br><br>Does this sound reasonable? = I am missing something? Any hints are <br>appreciated=2E<br><br><br>Best,<b= r><br>Fabian Huch<br><br></pre></blockquote></div></body></html> ------O13XHIHZ65RG97RT6TUU0WJM0LJN5C--