From 54e4c7dc896732bafcd907b0380d59efa0a181b7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 6 Jan 2008 21:43:28 +0000 Subject: [PATCH 1/1] better documentation both with -h and with F1 --- matita/help/C/figures/developments.png | Bin 15793 -> 0 bytes matita/help/C/sec_commands.xml | 33 +---- matita/help/C/sec_gettingstarted.xml | 144 +++----------------- matita/library/depends | 176 ++++++++++++------------- matita/matitaInit.ml | 68 ++-------- matita/matitacLib.ml | 3 +- matita/matitadep.ml | 5 +- 7 files changed, 120 insertions(+), 309 deletions(-) delete mode 100644 matita/help/C/figures/developments.png diff --git a/matita/help/C/figures/developments.png b/matita/help/C/figures/developments.png deleted file mode 100644 index f72458940cfb5082d5043e713989269806535701..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 15793 zcmb`uWmFtdur4};;2PX53GO7g1rHtw5ZpDm`{1s@gM|PAg1coHTr#-(3=Hn>@+Rk; z``*28-TUjFHEX7O_wMQLs$F~6_f=I#tEeMvg|A z1zi}vltMf`AgH0?oni>S6nfd#WD0zZ5Z|8t=@yyw?*j_dY@pUzF$-~88t)HjbgPjZ zBZrLRosL|!(FeB01oJhUSqH&O1}SuUt-lEYVAI**J#bD)$xO}gYP9bw`Y?PA;ux?| zwY-5pgJ42^8IpJ+8mToCdia*grbUrPTam`S!_gN2z#Q8bMAORpUSpCM-{+bhH>V>! z(>|a$YhcZdf41dPBPBg6Y1`<5ufDFveS~XV(n1sYiUD~wz~PNuYx_i&MA^5y%Y8Ie zy0F|rrjYE$9!MeTTKQGijoZM-gN~9aqVr4-7s_Q}kZ$3ul8S+qlp=(Qj?C-zYsJT$ zaLAMByog{|S0jI?3rrA~>g;J7kO1F&97CdtjQpfip#3$bLCX56h&5T@2oIT$?%@+_ z)!04K)RuBL1X&oiwhe~8Bh-rVsfb=8I+R!N;Fxb>t@6%pGA|p{_lsxfGk!z#BjB8_ z!EuE`l%{$-6ghDKEfL-cKkYpAp6@V3Nv_%9d6|2g@_XYW&;tqZ&~*Ju5BIWvN5|FK zvjppnnK`Xj1w4H1(EpWz5)w;3J&O=E(%FEX*lhbCXFs;1}CU>7$Y_qo6e3$0|1{N1pu%{+5Tr) zS0?OTiYP`8svoK7KSoFTa_=z&12;KG#fE>WD%)Kkh3z5*?Yi~lK9c(N&~iOjKo7e3 zp2pxvqDEcL!e&e}huE6b9ymb)2ak8J`TPm7kuFV+$wR6m-pP)FrfzKhszrU&h8MfI zovK#jIxFfX(iVE(xH&O&qx$^(wBN3vj}%2r0FaD)RRsv5WCP2rv#^M^C)O^e7yG!E zE)g03Sw`2rRx`a@Du0##x@#~I+#iLMOZQ~@x~U{n?K6{7sX`2;y39rgD|l$5Pk1lFLxg$Dc#h=czK8;9F8>Dit&eqmfe9t> ziJ%7!jon&5&yE$Lmnm95`78kj&;TcW9zi)GNecqf&!+M8>p^|_{;}-_0nFJ=oqbW1 zl4?#3)c7Hm`B1sp9(0S{uU)HNqI<=hA0kSaZluuSD&7Wv$d9%xA)vz~Gt<<+I=YhG za_MBl>DmtB$mi$}h^Nh=XzcDlZsy@`dGCv(X|}|Rvw>R|VjFmWXT3ae*HiXM{y@x` z5;;U4Uc5GX<55O}DW9c#FHyA||3+6ya3+}uTffm6<6AKYtQ5byldSizdg*Jg&JII) z0Q045#q)){!NhbpZxQJ_Z@e)lqlY7!)--2JM2ETsD6?Z5+VugwpN#h#Asy}!R`eti z&mMcloh?U_HxBQZ>2&hPG}hH(vG(RoKk5CznYrcs zy=})^btQ?C2Te5P6aZ6fB9W57+pu~=g592496VS;@;QqI=0XKP%48%EB990Bn1;A8 z8=`ztK(=WV8n<&h!)pKVXRmr`OmjB z4P*4~C_jkMNYlq2uwulkQ1=bB(w^uLQ_-JewTW&lWfuFYF3urC!2JR?-v(}{OqEPFWLu7Y| zsj?p)@4c#aKfJSnN49^8uk+*XizyYo0f4-`PNvgVM2HW|q3aGAY-8ifLJG@)qzd0?{4zM3#dhT<$7sCnJLN<_V^he`_%yqMLwm*10ZG|) zcmTfaQG3yLNw{~}J%Ehev9L9(2?vtjqzp;U(pwic!A3!&{57>@QDi2q%%ENQKqCsm zeTo-0e~L7x{}e&@xXd^x{asU@@$-#?D1cex0mm2Fj8?oijV&Xe2$-VuY^8(ZO{Jl! z(b>5(od4O@6^(SzLgU8I@5eUQp042T6C=(3nQ7b)ZHjo_-eh=~1Xn?}$I@2M3?3F|2C)vN zO@FG5Kb@QHsy=_i1;hkStFgjEDy zNwHCpUEQ=4J}M0yrrg)KLQrKG`Jw{ax_^wyBrMLCFmZt+3JO%XT?_=6EnjR{Siasn z5~EsdLM_`Klhgo5*3Q#PU^sl?Lf?GB9g4~J?Dw+6Z!YBU=R1ciV=cjO+kHoq&ygfI z>nn@+F221IF+FVvY_okifIs8p)N~lo%7o^GvyVdSCFDA(S>v$DVBhu~(^OIN1@WdH zZ_7Bs?%nWO{1cyIM>Zgh%CY}kiIMykh;rQOS7H4e`y9sS^Rs~at8jA@ zH;WZ8hG7+EPVXy?WA4GPt$M><7w_$qx)4{I@7*hKPJ+ijFE4=qKJLuI-j|KXK zUs1~gXA+aP2QTW+VzxqA@TKhCZJ|zTpc@Ib+rIp#-?a2IR1UFWN!@vhr?lhrFGZR- zO58DgR709L&J^xqVHzKo3ll8<~BqOP~nU}8W(R@T=vvXbcZVbkogqYu?N zVv1!5=t@7MkTPrfmJ|rsng5FZRu<9!8Cl-**~o&-@QMlXFFP{UC&UJw7>GDIO#SrV zvHzu^;KBMtHK6;Lm9+O}e@$a>B|>K?&{6n!ETwokPp*m>6qqL$_z65B6_icwEozju z;-noBc=>M5L*=&{Vl`FZ=?3eD-Z_nwo}C*lcp7NY&z0~b!l6bXiFm6lHz~VXwLe55 z9@a|Y#L1>wtD}%YW$57;S>a#F-yosvW0SoRy6@MnH4W9Jn62XRKB8#_UA6cEi;Q_v z`Mwm8&nx=|S)&hFv<`>QrmWv@+oa#%ca1a)iR*d&8oXhe9h1!4jv#R5zWY^ zik2n3@BG9bmaAlV5de34V}tWnRfKI2<2Xl=nb){22fbxz*;zzKJ}ov?$#Yqe3Vz*d zBcR(=lR~*&U`}W}80N1)#Azd8!cb*lH_{w#IW;~!M=jNXf7CI;ZQfVFu++V)V*KMP zgl-U?b!<&bNoaVCT z)6f*xROJ=0y3n!f%lvR3zj+8-HA`D)Kvki7NDYjdA{&lSJ89_g!sCN9a&deG|BlL0 z`VReeSGnu9xx3VNIY6PgovQfOJg&B(NS>Wz_m#+>ec&(wJUD4H-}1I*KqJvML;_mPM2WjA>9tMa z^zWoXmf++~)FBPy&Cl@SmHNAXFfCVcincv`SHNq7zvRLjvT1X{&c^aR;MvN2i>9r? zBxk46JahVOoPz{)-)Ft|?QU0UvlFs^`<=jFXA?q!z^2D}kM!c%+MEV7`x!ruOv$|g zgBQvXC9BpFs&=EIi(Fip{7*Mb%Iue>O3%WOx@ig$KL@;hZKcs)PuJsne@F)wuLQ=m z`d4+^Gu~R2W~%0nIOeYO{KB&}{ioS>_J5iUzy4@BGCwJ*r!S{J+g{AhUP-F82#n)W zuS2sl?5Y`5S;?H&9d2{@W5}(X8yFUSxWpYGbX~l8sIxh=kbcXd!olhQZEC9gTq5k{ zJ@<@h_b@sl!CR~`#9DMS_UD^DzvJ1A?r_y8QN2r`f0FH#^4^S#a*>Uh$D+XAVy)J% zo=c$$5Gb=UcI4+@*}s*E^{JHssg|>N%}iUF@r96h3;zPQu45-3=J`0Kk5=$EhTlht z@|?08>)(pEtBXwZuVKhWp35GgfPp*k&R^6~?gcDppNN-Lkn4Y!{|d2z_%=7*@b%BPHy+L>h2DnijG?ywU12=X8$nghrH{Vt;AQ~lIgoqJa|jj-!^X?W%&kVK0^!*SvCYu0pGvxIFE-E8mTTtvMf6EDDln(} z&yPogZn_c=TsNfCD`!cl7Un%IO3bB2m*;n}-y`M|d7vWyl{&i?r-tLUxXmzyikSYd z^?bcjbTTjet75y7qAS98cbM5;`b`r3WbIyowE9gZoPHiQTwBFSbx-wp^ACS)^*4uR z7G0O>#%e5EivMG-S6ojL0ksyz`$>iCzcl7OjxXkdJlRLTpeKO(m-RR;g=fTmrQX-E zg9;GCL%dRLPi~ZV+h|FJc>E^inX*x_#`Whet#b%H%bd7{rw60HAva5+`L3{Zff9?G zeMbf1`Iz&pcRx$|Eli%V3C~i<7x|wA$c9DsvIP*krh_O(Z)VKVVa&VpG+kNF`wWjr zAyA&!J;R+#*|uS)i?UAtVYPy(qS)w-lumZOfJ6Czu2otO93zE|mJOC5ec#9RSuFE7 zm5NFeuH)rSBHY6-j)5Z++jX9}u1${H0PXhkSx}%w1`WXmm}T zf67Y`&$zs>?@jk8@6ii%iT+K((tHr6qP#v|sVvg410CSb@*{16FH^&toS(R6`wX== zBEWS=+=QwDqjuqOX6>WP7P@v~Qx+w)SZK|4&3EruT~>RjdJiJ&uVW2j8ZGa!b{|QW zJZ}h;#wK`k_jp9we1ub4aq4bwADaHAls9fxm985v|BvNlj>{3m-T&q0n|go7i7teT zD;o#=Agk1$akh}Dc}m>$Z<%IQGj6gBjD-xOyHqqfL3p)Fgs-P#o`FgwHH_kpabs}4 zZC{o7VJ#;6J#1aPC-c|s{FYZ{NN^0x3Zov+gOvC3N*>bk8(d=KY9?cx*0!at$*%3( z?JQrpPd{gQx!-pH^WUF(TKXr98Gy3uY$3Rx=W$bb`i~Bcdr;kNda2&LU`$%9@25ts z+XNbNxU4!keeZuEmKrzUVs*Gs_ZWU`)Q1}W-VF0qe)Ohlg;w*#0koZ*Um_o>?c>H_ z+sgL)hEyPNHhm)f(sB1PR-dcC9P62v#<+`La%3Vd+6x_P)vhMq z&YsA=!+v2BG`K|^sh^{u1ogJ7Uu~+id{#6$XFRgMdyIR|zRL$8HfpzmTtH3=jduQ!)ST$4^-P2j2cqz5nKmJ-&s42&2KxP6h7h^t~al zP5@@GsN1V%1|=~S=!YH{oYVw#vrYP>M#|1LgEgEjR69L|Fg-0kr!AS65$}rW2HjYm zEXzjH5#*BS`Jua7dvku-d%dR}MIysW7!kr&RKE5I6Xhx{tA|7V(e`z!JN@{qGYlTi zc|r@6`Lt$t|Jm-D{hobUEVx8RtXC`wVZwQ__43!Sa7W~VPn#t7d z-T%0i2lSb^YO3i7*`e(q|9G@={{+ikA>(n#O+MohgTCRJuX?O_;W^ED!Pv>g`*ZJ% zSw5SsuoSD5!g-T|S_0RpH9~E()=%Mk6^(5MM|{t9G|7l*PQS66dz+!1ybkpm=SB>~ zD}+8vlyQE$*4d2w>sI?{yLWIm!#3_UUc=BMgn)gMlas@oS(C<>ufvkoClH%4Y1s!Y z@c$r%T=(}kC`7lf0soknPoUB7&L(dnrhisaPb74%mH<@vPa+qkR4I%ga``_PQwjdV zhAe)Sq#8V6CH^CQNqga|=l{6d|7JoL*%5r6CFdi%82_#H-m?$AkKn}H|8E3uu|KoG z-;A@$nqgLt(=p=$7Z;cJXI~@kaVb#M)YM|xYJOQuXK9G1Qf?~UrgPLQ8b7G$?37@o z&$XlpIBoTY5HqL$Wug3=dRDN^Z2Y%*IZNwq9WR0HOTqioZ=*K?&@O})xYt0osW_I3 zx9X0mT$}nlSz1@?V=h#JG-v>mVfEKKbOZ2C7b?sD_dePRR%zgyP-HHrew>K!tr|X5 zXt@8s?v9&KKiBDQ%*xNXs*zz~G8PtAUmWBZQ@U10a0sG{_NZH3s7!VTE5q!SH#asI zgx-=v(knZm?VcYPk|nF>q${-xJss5iAJ!sm7JdpH92|7QXX4cS(*>rctVdy;!J%L7 zdhqb0dv|8)(H0{jep)9UIeU1Z=_5>yo*Y6IB({R5J6 zbK^5J$ts?0sSy{WrU-v0*AqdHZaa_P(IK7$*_;UsWp?;=OJ<(Q<3>W2s)$WBjz>d7 zGvD}CpvmDGnV{??$oDG9fU|lMO~Z18iIg1#JG;3f;450%#OqZ*G=Zu}>B`Z*AHe}No{wDf_10XA5lz7g%wY;|et)`^ zk&`ps{dudP6xEjoA?0z~LemlswO*-K?pu!Sy2T6NZb`&0H?^1Od2*OW{9V6p*PzJgIhVcbzp@=_?o>%YUA=y1-E<3CvEP!gy{11|%}Y z?lp&>@5(8f3lS)@jrJaW$?G9B5Yz_0s?={G^&pAJK`*jilD3$m5K@QVCi8=kvhykl)WtFDRF$-lHkMaa?bDwyN)|go{3JIA`mwv+k_~yp_NYtj`JA(s7CXz=0^0?iFaO~Kogz>T)@guXKE87+$ zsnP;>g0$o#puve2v$&AZz(92E5RNASrhDfwiI4QOs?K@{+uMsm%=r@^|M{gMdZM$n ztvzfn0eKl{Jg4WvIc;E9{5V5}h@9F3I+zBXYwAo4!VXEXeUf$>59LAjJYJ2jsIYIa zS;YqVl0y|^d`|EY8CKl|-Eo`u6fm7iIhR{rlf_rtoVu-^ z&ZMj?3~G1*@Ord`(4|#sZt3tf7!I0?DAa;%onYAnC28k!UsU4NUV2Zv?JE(_RAUbZ z8Q$Z5aM}(=fmVmeQ~?IOB=ypf?=C2VOr?#xe$c-zAQ6yMWYXUN?i&r3}HgwlHhI*k9IV@A4vH<>CPV)V%*{0eEszUA(GIrv&&Wyy~bE zIQKQLL>-1^y9F(WO02IP6#_2+)}uLcV|k$Q={ah`)$dVSY#C{O0gu;*Fa4cmLe#93 z2bf}C6r}FFa)UDj>Vwdy`Y(EaJUryBdFm!V?kV1=h$;_BK@zB)&ko)`bhzOeQH#H< z;#5^1B;HvqXYv+Ba^F)P&RRqX91RLG7pwu&UL8t=wC0cWz`D4k-w^2@=pYm^Ji_-y z(1RkP6jbXbS04kFQ(8Ly%k8Lp&QTH2-bBW0|7J8#IN=WI38g2EvoY>|{J`GiZrW~w z%V%aS0=#~o;4@+EWBmvdZP4nAWot`by6GrgLJ$QzSPLC}3>dGq=2AXdq}F`ek2yB} zZD3_~7OrHD||4lC$6Yc6*O{~aCbYAt`I z?t9bKH9_vWt>=yZ44`a2>Yt|%fE{eaiHjL`Lmowb2J5g21_%>yMid5TAmzuo_7}@H zt{oHwvFd0Q-DF>}94Fy^x!7m2Ia?R#j4Qb&ZXupQWAkl)|K3>==>Iq()!=yl0#Ot) zf++!@67&4Cc%h_USC*6Ur~-wsFrVEfKA2etb^VC^;1u+snycl&iF?PCduMHDCklgb zwfD?Y0@f~z#bZ5M;(a*df{%II5+Fh#oI6@!2*6i(QS0f590$CdO z#3v&Pu`+$+0YWyJ#vVnnIqsc!D2=OCCBM{XB>kAp#(6GvaI5f1)!JyZZyV}!r|3^g zDVLHmqhes-WDtE2r4fw^mP3rmSg0J<#_tQ*Y470ZEKK!64B=@}*4EYr2M0s6%Nvs# zH!a72&QjLHPaRCS0j)h-_KMlX%|P|81>jTRyK1dGWffX~aa!83@6or$0l`R*cWdFK zMv_yE@jSlM%of|fosS-TE{+y(a)muQn+}(11L2JRyw;poPtCMKLP97`A9W$AozY5|udwBWaw~k3bNC0D* zF@0VIV&y%X-YT-|{dqZ{mc!0_m{o7>0+*9XUIPMKh(R6M7--_wr|)}KbwBNOq&}+` zulDT;5stTfK&NQf3)7L%3zmsrWgo*@$}m?rCVfRV4G4~xIz7{Ob9t?#N#DAQgBm6; zvt}g4n6o0<32>&ubCnm6VcJ~JsBFg%I2K>^cVke^>4=VP?lbY12T0nty%f;c`{|JJ z3LV=HT|Cjc(KtHSS2D#7^f>?%kl=7f0TOPM|0meaJACMa(SxVGu!GgGsWSO9=J)rG z*kDwZiCU;&#l!yZ1$Q+*=sFG3Q{b0BHl`mYjKQbY^;aZZdNz&mbypDc?5#qblB<(y z+K}{IR9LyOYPOgYM}5rV+&|b&Irb1Q3vD=|j6*|4h2J;$BhexN<;ls3B*^zt9UKTC zausS2rp88vWLW(1^$%amV&l2~B2`+ZsGr@RzGGnEdTOpBebw-R<_Cr{*3dqc6b zBY3Yhx+3X zi+4_5Ols=OH@y;)8tc-%eSNU2N=Ve70OE-Wfmg)D(Jk_)-bDFfH#gX&)2Lw{-UZX; ze|c=MT?wCSgt8~Cd<1xZ!k!=Gb&bm#vPkl@S<@J50s-RR-y`#tfbfuvgVHPYetK0O z+04`78yV4*(!xU9Jof1tRQNWwwqQH8a0N9WHps}>6*&9#gn5sE1SEmv=)kBmXhj4( zP>Q=bqWI7~$`Gc@RCfniT@Q&IxL-rzS9WTt8?%&jiEt z{oB2Hs+QYgEZKC{hZo$erWRNZ=u#jt4cBhU{6<)uD@z@c5c6of)lI;lu!>>kfP=6w!-o*zm6NtG}0C$=0KKVbd#fb?7iXo*QA#smkaY&-8yvOHYeepOhK zxX#+t|K?&YNBr>c)Ig3R@%*&JWi>`z!v1*Hm8a|d80oC6_rTU&ZQT1$MSmwTGFt^^ zw}x5mjdgYroZWFla#h!%3%UPit}*Nq;gx(tpN2-bP(x3#V|dVCzBsw{7ZjZD8dXI~ zhz!{tUJ5wVbE?t}LDpnq&?|1ddAPI9=CQi8irc4pQKk-P4!Zi%v59P-*MV<>ZHDlL zyY`(Kq~FeeO_;CEk@6g8EC}9TdU0*{%7 zn_6g}K6(9^+5I#JA=J&vf}P*m;1i*zDO$2Wg>MZo(Y3(VD5qZ@`X+SV)qCEYMt02B z3s4&kk9`%tBZSX#b;r^-(ywEwH-92!hjRbUJpBD|`)9tG@0UL}r97vsRDN0vp7qGf z6ta_{4B8*pK{VsM9A;)_fc~V+%&6A$4oPQqx;-BsV%z;-IW#AFaPJ(Orm-3J8j~js z^i)YtdiKNls=qwHO6~v{JF@t&HRp7qq3INbLRIv4k?e9vqsYkk6MgGjCMNhz*?H+c z>1SuPXhd-tNS|7UY1?E~Cl6buV&VpM zmsy)%4{L9hP^=Df#9WBDJPysK8Z37+Bu4M?;QZ{eiHt`0+YXUz{BgZiK3^S1D}G*i zXu-vvACB!g{UcJJfls=DMz!0@dDcE-2v)JvvJH-QinqWsZiq6URQ4hyfoc?19wF}NvG6Xzt2qNdim#nmbGpKowbGJ z*sc;YR%%BMkS7*sly$9nTk+Bw^gU5h^Md~%j?PA@f+WFClm91*?Iay zeX!={eiL?jOZITq$&e3B>cI%PrpfFs2gQ_HL@HMV8SL;S!KE4;qWARF54j&0mF$``Sy@agH3o|#Dn-{qv!-fK zw?~}a+@uqaxUw2G<==FQ#p5Co?6;RrUc6PAbzr~s$9NJ8#HeKswzVpiY|xNOP#=pD_<>C&ybww8oE>>Jh_#WDOuUihznrI&r%*{)`y&pD*G)FC zU*fqCh$4Wz1uo%&Wgi6T);b^u9mD!|PTk11@^O1A_^YhOzLNJWoP2eDb;b^&P4?P- zHY^&+50)7L9NeC$x!;?Kbdt&WpECFYZv=ilE}}qa7vP`8!Z$^R9a^U?O`rPA=!*z= z>~6goSa@DFirV!IeL@fKrirJV>p?_m){c(iQd8XlL5jr@xw*rxetj0^tdCoagUe{? ztOy6GyS%?7>LA1$A06FwCE;bZbR}VWY?3%Q$oxmx6MNLSCCG85t-xmrAN?hjyDu`0 zSWIML;cLAHY*`JB7ouXz$$3v?EG%V%!-HYDQlGj-&(<_V@ST957tm%hyc%)sdM^I_ z2Zx_0Sy{W@#53ENpUOW+wYZ_JR!XnwLcM#SL$6CrO8nxg#c3kLAx&!sSyNGe+()lw`V34=q=*27Ix98iBDt1Mf``BqH#j=>@==!MZgP^|+@%siR534#CZ4C7gpLyQ z0S5}(YFcSELTdf^mLQJo3ez2I-#-BsC_IjuOV0Wp)o|knvwZv0us&kv;g0m=sw!4# zdvxugE7aTn7?(yoD)fVsWGv}op$E9bX5u$7k>`~xXMjAk&9Rk;C$&Q@>(Nmky#KUd zMMdUMfTm{Ll~yQHqe`UrmkkR@&V0L8wA9<8T*czoa=5e+KNdab@9)(HqjBV8+c1@VzEa60QbZ)l(JQEY?3vXn zhdsk^f4%fI|A44{`{{%4|N3=}%aeeh&%+y6tyca^wyDUWSzP$4RM*@lEfHDXGM>pFyv~abqY?T77Djd+8Aw9B^VG$bCU z%$EGckh)f>DC24|skI({{W)n}zJQCJSK8HvXo-4`h|uRN)qJ7&q=*kT^W5lm@f2BE zSvxZ&ctox!1_n8wpioLt)krK-Rq4u4p~$f9{ZKi29J&lh#f5;FhMAMuWrY`vM7Yu9 zrX7ds^k`21)%_QgP}T4qwn*-PjROKt5aUANDjH?K+CcD0mwnzIh)Y`bPMVSQY7wzc?-}I4lyQj7;Ju+P?ri0@+3?R)(~d17C>_Tl0ym^s%I1K#! zlM)(KbJyW)vw-SKON-via3do0qgFfqgm54^HPr%MAk5~G&wG`NHcrvt?fr<)7=KTW zycOTLcF?XQzpU^7pxlW?O_)1{M!>8|P$Wj>< z6_<)E^Ogy4<_MVHzwGxz#)M{m>fTI=fNRq=$desqiyklEs63obc>0S2S$`R{#~P?& zKPRbU10N~t`S-4XX!cK^{e>3i>|35Qg_1ad$n_!Au^ohW)N|Uugv`SwgoWDgyuH;p3DPF#8yOq~m{XzR1(K7F=J&L^ zk&c7>yk6ei!@I-TS^^(YEnLY7*5UXxfz%`4--YQFcD1@?z_gliH8iG@zkkPURYooQ zVqlSX#y0{y9$hWQT?Djj_ zca5cxz^6V+pL+T;rsh5E2(0<#+?|bJ4h@`H0^e5|MoB8#@$R)Nar-(m$qe+q9tR_` zYd$6rDAStZ7$IT*W!F|^q{~|O+uv-9`(?g(SbXh6%n-|Vhkt^+<@B!3S6JKQaGL~_%Kx``$e8|R$r&~`!wm@=TUP7CZ z5kE*aV{BHu(Kke*BTtmTX`r~LBV8gwSuZrp^ho=D<@$AKjm2(crpsFj-{2R)9Njf% z*JJrU9VifyE3NtMN7Lr10X+InXtl{hMw@597uL4<9yUAx8_JR6^d3BUrBqF0Y^HUF zkWKW(aj#g!Bp(17svCi4eAXaTAG0*4b++zwb*q9U@M*_g*rri$=TaCR;Vav{_xXL;L!8oNX(U8NY_TVx@~npQJ*|0Ua&f7a3N z14|uCPGjTg{$+kbz+;KNzl#1WVxikSzm1BC>F!qn(;bAX$I%LqI369{>{o;FNl6o* z9`Dyjb8T{j+-OuN1o|i7);}ifCV1GfPN5|gm)d>`vWGTO8-etmj9em(N*(fgtiVM5=4p7!!kq|k|CY3U1Ek(Xw*=z7Q} z16|I{skkcXCxUVM4FK7&q@o|NFi$?Vlpv#)2UARK@IjJy9EV)!|mp|9O-c@kfGX#P>J1X|wCw zxh(S(%9{=EB)>fp`Mboml=wXuEI-1`uk`gl+@B)x^UuCmdI15_*49?;9gi(E0iW<( zxFFe?_^9$J-^t=FKK z!FaYDB=ef)W_e#PXc>L$8V3qe7 zU)I0j;i37IEI_w$em2{B8UlQxuB1XE!&d7!9W>z%^wV*5C7`jk_#C~iwaC>3JHK)E z@(5R8?kSWXQczY7Q!SB}vm$w?M@__-5qyRhbq4m{S_R45%oe>BM9AeM%XzC4-u?8B zck|R6k-U{Tw^DJr+2Pq~peXt!CRb8}iwLQaiLb7fYPR#gA>jG*=MO%`A_X~l7C!oo zv%7oPmp38m%wg)x>}UK+mctD{JCuuM&#lxG1F1 zQe%VuUWEQl)726@9|OlusqbV@{IQ#p^R!~L8p}fzp0dRajKvXCp>8}vHbHMYe`tTD zOZ&TK*zCA^{c?xx@NfMluFljgDJIH45y7hgwTEL8HI6IC2qDJz$foUx4GeQTw<*WY zj#mSM+P!EQI5{y8IY5x#h1?ux?vEr0-K*#>_$jLg{}`(#0KI}Xi2PVhu6>-pg_<0r zpKLL_DY(9#4}oP6se5`N^f==}R+104P7gb2l5~K?0lp5S)g`qVp8WN&Cdcsc*-B@a zIwA)iN6UtTS&^6&frHs!#u-q-;Kny|y!rHn#0B}@2`Zm4gWAg|>(`hck6$1f7=ZmYhLEkY&rbxSq5=`I_KhA zT39I1=I}yff6giD+@w7-~XT|i*&|EWmEG>dwrnb4eR^mhgH5D!lKdq}yYQDH&-S1R7795WQNzYzWZ zP-s~8?Ij>7k17#STBJdNCjMU_VNmJtO^at^BHQ=MHs!WxX HNyz^Ld%_o7 diff --git a/matita/help/C/sec_commands.xml b/matita/help/C/sec_commands.xml index 5e55de999..4fe77d7b7 100644 --- a/matita/help/C/sec_commands.xml +++ b/matita/help/C/sec_commands.xml @@ -254,8 +254,7 @@ On the contrary, theorem and definitions declared in a file can be immediately used without including it. The file s is automatically compiled - if it is not compiled yet and if it is handled by a - development. + if it is not compiled yet. @@ -282,36 +281,6 @@ - - set - set "baseuri" "s" - - - - Synopsis: - - set &qstring; &qstring; - - - - Action: - - Sets to s the baseuri of all the - theorems and definitions stated in the current file. - The baseuri should be a/b/c/foo - if the file is named foo and it is in - the subtree a/b/c of the current - development. - This requirement is not enforced, but it could be in the future. - - Currently, baseuri is the only - property that can be set even if the parser accepts - arbitrary property names. - - - - - whelp whelp locate "s" diff --git a/matita/help/C/sec_gettingstarted.xml b/matita/help/C/sec_gettingstarted.xml index 0066449b0..3b9af3e30 100644 --- a/matita/help/C/sec_gettingstarted.xml +++ b/matita/help/C/sec_gettingstarted.xml @@ -88,133 +88,27 @@ Authoring - - How to use developments + + How to compile a script - A development is a set of scripts files that are strictly related (i.e. - they depend on each other). &appname; is able to automatically manage - dependencies among the scripts in a development, compiling them in the - correct order. + Scripts are compiled to base URIs. Base URIs are of the form + "cic:/matita/path" and are give once for all for a given set of + scripts using the "root" file. For example, imagine a directory + "dir1" containing a script file "file1.ma" and a + subdirectory "dir2" containing "file2.ma". A + regular text file called "root" has to be placed in "dir1" + ad must contain a line like "baseuri=cic:/matita/example". + Then, running "matitac" from "dir1" will compile + both script files, placing objects defined in "file1.ma" in + "cic:/matita/example/file1" while objects defined in "file2.ma" + are placed in "cic:/matita/example/dir2/file2". + Before you can compile the scripts you have to generate a "depend" file + running "matitadep" from the root directory. + You can divide you work in many roots, just place a proper root file in each of them. + If a root depends on files living under another one, you can add an extra line in the root + file like "include_paths=../other_root1 ../foo/bar" and "matitac" + will enter these patsh to eventually compile needed files. - - The include statement can be performed by &appname; only if the mentioned - script is compiled. If both scripts (the one that includes and the included) - are part of the same development, the included script (and recursively all - its dependencies) can be compiled automatically. Dependencies among scripts - belonging to different developments is not implemented yet. - - - The "Developments..." item the File menu (or pressing - Ctrl+D) opens the Developments window. - -
The Developments window - - - - - Screenshot of the Developments window. - -
- - Developments window buttons - New - - - To create a new Development the user needs to specify a name - - The name of the Development should be the name of the directory in - which it lives. This is not a requirement, but the makefile - automatically generated by matita in the root directory of the - development will eventually generate a new Development with a name - that follows this convention. Having more than one development for - the same set of files is not an issue. - - - and the root directory in which all scripts will be placed, - eventually organized in subdirectories. The Development should be - named as the directory in which it lives. A "makefile" - file is placed in the specified root directory. That makefile - supports the following targets: - - all - - - Build the whole development. - - - - clean - - - Cleans the whole development. - - - - cleanall - - - Resets the user environment (i.e. deleting all the results - of compilation of every development, including the contents - of the database). This target should be used only in case - something goes wrong and &appname; behaves incorrectly. - - - - scriptname.mo - - - Compiles "scriptname.ma" - - - - - - - - Delete - - - Decompiles the whole development and removes it. - - - - Build - - - Compiles all the scripts in the development. - - - - Clean - - - Decompiles the whole development. - - - - Publish - - - All the user developments live in the "user" space. That is, the - result of the compilation of scripts is placed in his home directory - and the tuples are placed in personal tables inside the database. - Publishing a development means putting it in the "library" space. This - means putting the result of compilation in the same place where the - standard library lives. This feature will be improved in the future - to support publishing the development in the "distributed - library" space (making your development public). - - - - Close - - - Closes the Developments window - - - - - The authoring interface diff --git a/matita/library/depends b/matita/library/depends index 199b1e9a7..40cddf02f 100644 --- a/matita/library/depends +++ b/matita/library/depends @@ -1,89 +1,89 @@ -higher_order_defs/ordering.ma logic/equality.ma -higher_order_defs/functions.ma logic/equality.ma -higher_order_defs/relations.ma logic/connectives.ma -decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma -decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma -decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma -decidable_kit/fgraph.ma decidable_kit/fintype.ma -decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma -decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma -Fsub/part1a_inversion.ma Fsub/defn.ma -Fsub/defn.ma Fsub/util.ma -Fsub/util.ma list/list.ma logic/equality.ma nat/compare.ma -Fsub/part1a.ma Fsub/defn.ma -technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma -Q/q.ma Z/compare.ma Z/plus.ma -Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma -nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma -nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma -nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma -nat/euler_theorem.ma nat/nat.ma nat/map_iter_p.ma nat/totient.ma -nat/plus.ma nat/nat.ma -nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma -nat/orders.ma logic/connectives.ma higher_order_defs/ordering.ma nat/nat.ma -nat/map_iter_p.ma nat/count.ma nat/permutation.ma -nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma -nat/nat.ma higher_order_defs/functions.ma -nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma -nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma -nat/factorization.ma nat/ord.ma -nat/lt_arith.ma nat/div_and_mod.ma -nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma -nat/gcd_properties1.ma nat/gcd.ma -nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma -nat/div_and_mod_diseq.ma nat/lt_arith.ma -nat/times.ma nat/plus.ma -nat/le_arith.ma nat/orders.ma nat/times.ma -nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma -nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma -nat/chebyshev_thm.ma nat/neper.ma -nat/gcd.ma nat/lt_arith.ma nat/primes.ma -nat/minimization.ma nat/minus.ma -nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma -nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma -nat/binomial.ma nat/factorial2.ma nat/iteration2.ma -nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma -nat/factorial.ma nat/le_arith.ma -nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma -nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma -nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma -nat/minus.ma nat/compare.ma nat/le_arith.ma -nat/congruence.ma nat/primes.ma nat/relevant_equations.ma -nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma -nat/factorial2.ma nat/exp.ma nat/factorial.ma -nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma -nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma -logic/connectives2.ma higher_order_defs/relations.ma -logic/coimplication.ma logic/connectives.ma -logic/connectives.ma -logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma -list/list.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma -list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma -demo/power_derivative.ma nat/nat.ma nat/compare.ma nat/orders.ma nat/plus.ma -demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma -algebra/CoRN/SetoidFun.ma algebra/CoRN/Setoids.ma higher_order_defs/relations.ma -algebra/CoRN/Setoids.ma Z/plus.ma datatypes/constructors.ma higher_order_defs/relations.ma logic/equality.ma nat/nat.ma -algebra/CoRN/SemiGroups.ma algebra/CoRN/SetoidInc.ma -algebra/CoRN/SetoidInc.ma algebra/CoRN/SetoidFun.ma -algebra/monoids.ma algebra/semigroups.ma -algebra/semigroups.ma higher_order_defs/functions.ma -algebra/finite_groups.ma nat/relevant_equations.ma algebra/groups.ma -algebra/groups.ma logic/connectives.ma algebra/monoids.ma datatypes/bool.ma nat/compare.ma nat/le_arith.ma -datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma -datatypes/compare.ma -datatypes/constructors.ma logic/equality.ma -assembly/extra.ma list/list.ma nat/div_and_mod.ma nat/primes.ma -assembly/exadecimal.ma assembly/extra.ma -assembly/vm.ma assembly/byte.ma -assembly/byte.ma assembly/exadecimal.ma -assembly/test.ma assembly/vm.ma -Z/z.ma datatypes/bool.ma nat/nat.ma -Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma -Z/compare.ma Z/orders.ma nat/compare.ma -Z/plus.ma Z/z.ma nat/minus.ma -Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma -Z/orders.ma logic/connectives.ma Z/z.ma nat/orders.ma -Z/times.ma Z/plus.ma nat/lt_arith.ma -Z/moebius.ma Z/sigma_p.ma nat/factorization.ma -Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma library_notation.ma Q/q.ma Z/compare.ma Z/orders.ma Z/plus.ma Z/times.ma Z/z.ma algebra/finite_groups.ma algebra/groups.ma algebra/monoids.ma algebra/semigroups.ma datatypes/bool.ma datatypes/compare.ma datatypes/constructors.ma higher_order_defs/functions.ma higher_order_defs/ordering.ma higher_order_defs/relations.ma list/list.ma list/sort.ma logic/connectives.ma logic/equality.ma nat/chinese_reminder.ma nat/compare.ma nat/congruence.ma nat/count.ma nat/div_and_mod.ma nat/exp.ma nat/factorial.ma nat/factorization.ma nat/fermat_little_theorem.ma nat/gcd.ma nat/le_arith.ma nat/lt_arith.ma nat/minimization.ma nat/minus.ma nat/nat.ma nat/nth_prime.ma nat/ord.ma nat/orders.ma nat/permutation.ma nat/plus.ma nat/primes.ma nat/relevant_equations.ma nat/sigma_and_pi.ma nat/times.ma nat/totient.ma +Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma +Z/moebius.ma Z/sigma_p.ma nat/factorization.ma +Z/times.ma Z/plus.ma nat/lt_arith.ma +Z/orders.ma logic/connectives.ma Z/z.ma nat/orders.ma +Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma +Z/plus.ma Z/z.ma nat/minus.ma +Z/compare.ma Z/orders.ma nat/compare.ma +Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma +Z/z.ma datatypes/bool.ma nat/nat.ma +assembly/test.ma assembly/vm.ma +assembly/byte.ma assembly/exadecimal.ma +assembly/vm.ma assembly/byte.ma +assembly/exadecimal.ma assembly/extra.ma +assembly/extra.ma list/list.ma nat/div_and_mod.ma nat/primes.ma +datatypes/constructors.ma logic/equality.ma +datatypes/compare.ma +datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma +algebra/groups.ma logic/connectives.ma algebra/monoids.ma datatypes/bool.ma nat/compare.ma nat/le_arith.ma +algebra/finite_groups.ma nat/relevant_equations.ma algebra/groups.ma +algebra/semigroups.ma higher_order_defs/functions.ma +algebra/monoids.ma algebra/semigroups.ma +algebra/CoRN/SetoidInc.ma algebra/CoRN/SetoidFun.ma +algebra/CoRN/SemiGroups.ma algebra/CoRN/SetoidInc.ma +algebra/CoRN/Setoids.ma Z/plus.ma datatypes/constructors.ma higher_order_defs/relations.ma logic/equality.ma nat/nat.ma +algebra/CoRN/SetoidFun.ma algebra/CoRN/Setoids.ma higher_order_defs/relations.ma +demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma +demo/power_derivative.ma nat/nat.ma nat/compare.ma nat/orders.ma nat/plus.ma +list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma +list/list.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma +logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma +logic/connectives.ma +logic/coimplication.ma logic/connectives.ma +logic/connectives2.ma higher_order_defs/relations.ma +nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma +nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma +nat/factorial2.ma nat/exp.ma nat/factorial.ma +nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma +nat/congruence.ma nat/primes.ma nat/relevant_equations.ma +nat/minus.ma nat/compare.ma nat/le_arith.ma +nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma +nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma +nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma +nat/factorial.ma nat/le_arith.ma +nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma +nat/binomial.ma nat/factorial2.ma nat/iteration2.ma +nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma +nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma +nat/minimization.ma nat/minus.ma +nat/gcd.ma nat/lt_arith.ma nat/primes.ma +nat/chebyshev_thm.ma nat/neper.ma +nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma +nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma +nat/le_arith.ma nat/orders.ma nat/times.ma +nat/times.ma nat/plus.ma +nat/div_and_mod_diseq.ma nat/lt_arith.ma +nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma +nat/gcd_properties1.ma nat/gcd.ma +nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma +nat/lt_arith.ma nat/div_and_mod.ma +nat/factorization.ma nat/ord.ma +nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma +nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma +nat/nat.ma higher_order_defs/functions.ma +nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma +nat/map_iter_p.ma nat/count.ma nat/permutation.ma +nat/orders.ma logic/connectives.ma higher_order_defs/ordering.ma nat/nat.ma +nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma +nat/plus.ma nat/nat.ma +nat/euler_theorem.ma nat/nat.ma nat/map_iter_p.ma nat/totient.ma +nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma +nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma +nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma +Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma +Q/q.ma Z/compare.ma Z/plus.ma +technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma +Fsub/part1a.ma Fsub/defn.ma +Fsub/util.ma list/list.ma logic/equality.ma nat/compare.ma +Fsub/defn.ma Fsub/util.ma +Fsub/part1a_inversion.ma Fsub/defn.ma +decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma +decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma +decidable_kit/fgraph.ma decidable_kit/fintype.ma +decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma +decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma +decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma +higher_order_defs/relations.ma logic/connectives.ma +higher_order_defs/functions.ma logic/equality.ma +higher_order_defs/ordering.ma logic/equality.ma diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index 789573c06..03de96b5f 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -45,7 +45,6 @@ let conffile = ref BuildTimeConf.matita_conf let registry_defaults = [ "matita.debug", "false"; "matita.external_editor", "gvim -f -c 'go %p' %f"; - "matita.preserve", "false"; (* FIXME, inutile pure lei *) "matita.profile", "true"; "matita.system", "false"; "matita.verbose", "false"; @@ -127,76 +126,29 @@ let _ = List.iter (fun (name, s) -> Hashtbl.replace usages name s) [ "matitac", - Printf.sprintf "MatitaC v%s + Printf.sprintf "Matita batch compiler v%s Usage: matitac [ OPTION ... ] FILE Options:" BuildTimeConf.version; - "gragrep", - Printf.sprintf "Grafite Grep v%s -Usage: gragrep [ -r ] PATH -Options:" - BuildTimeConf.version; - "matitaprover", - Printf.sprintf "Matita's prover v%s + "matitaprover", + Printf.sprintf "Matita (TPTP) prover v%s Usage: matitaprover [ -tptppath ] FILE.p Options:" BuildTimeConf.version; "matita", - Printf.sprintf "Matita v%s -Usage: matita [ OPTION ... ] [ FILE ... ] -Options:" - BuildTimeConf.version; - "cicbrowser", - Printf.sprintf - "CIC Browser v%s -Usage: cicbrowser [ URL | WHELP QUERY ] + Printf.sprintf "Matita interactive theorem prover v%s +Usage: matita [ OPTION ... ] [ FILE ] Options:" BuildTimeConf.version; "matitadep", - Printf.sprintf "MatitaDep v%s -Usage: matitadep [ OPTION ... ] FILE ... + Printf.sprintf "Matita depency file generator v%s +Usage: matitadep [ OPTION ... ] Options:" BuildTimeConf.version; "matitaclean", Printf.sprintf "MatitaClean v%s Usage: matitaclean all - matitaclean [ (FILE | URI) ... ] -Options:" - BuildTimeConf.version; - "matitamake", - Printf.sprintf "MatitaMake v%s -Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build) - init - Parameters: name (the name of the development, required) - root (the directory in which the delopment is rooted, - optional, default is current working directory) - Description: tells matitamake that a new development radicated - in the current working directory should be handled. - clean - Parameters: name (the name of the development to destroy, optional) - If omitted the development that holds the current working - directory is used (if any). - Description: clean the develpoment. - list - Parameters: - Description: lists the known developments and their roots. - destroy - Parameters: name (the name of the development to destroy, required) - Description: deletes a development (only from matitamake metadat, no - .ma files will be deleted). - build - Parameters: name (the name of the development to build, required) - Description: completely builds the develpoment. - publish - Parameters: name (the name of the development to publish, required) - Description: cleans the development in the user space, rebuilds it - in the system space ('ro' repositories, that for this operation - becames writable). -Notes: - If target is omitted an 'all' will be used as the default. - With -build you can build a development wherever it is. - If you specify a target it implicitly refers to the development that - holds the current working directory (if any). + matitaclean ( FILE | URI ) Options:" BuildTimeConf.version; ] @@ -219,7 +171,6 @@ let parse_cmdline init_status = wants [Registry] init_status; let includes = ref [] in let default_includes = [ - "."; BuildTimeConf.stdlib_dir_devel; BuildTimeConf.stdlib_dir_installed ; ] in @@ -259,9 +210,6 @@ let parse_cmdline init_status = "-profile-only", Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex), "Activates only profiler with label matching the provided regex"; - "-preserve", - Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true), - "Turns off automatic baseuri cleaning"; "-system", Arg.Unit (fun () -> Helm_registry.set_bool "matita.system" true), ("Act on the system library instead of the user one" diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index 3c3d421a5..a17845331 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -110,7 +110,6 @@ let get_include_paths options = let rec compile options fname = (* initialization, MOVE OUTSIDE *) let matita_debug = Helm_registry.get_bool "matita.debug" in - let clean_baseuri = not (Helm_registry.get_bool "matita.preserve") in (* sanity checks *) let include_paths = get_include_paths options in let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in @@ -125,7 +124,7 @@ let rec compile options fname = (Printf.sprintf "uri %s belongs to a read-only repository" baseuri); (* cleanup of previously compiled objects *) if (not (Http_getter_storage.is_empty ~local:true baseuri) || - LibraryClean.db_uris_of_baseuri baseuri <> []) && clean_baseuri + LibraryClean.db_uris_of_baseuri baseuri <> []) then begin HLog.message ("baseuri " ^ baseuri ^ " is not empty"); HLog.message ("cleaning baseuri " ^ baseuri); diff --git a/matita/matitadep.ml b/matita/matitadep.ml index 42034c1a8..cf1519eae 100644 --- a/matita/matitadep.ml +++ b/matita/matitadep.ml @@ -76,8 +76,9 @@ let main () = Sys.chdir (Filename.dirname x); HExtlib.find ~test:(fun x -> Filename.check_suffix x ".ma") "." | _ -> - prerr_endline ("Too many roots: " ^ String.concat ", " roots); - prerr_endline ("Enter one of these directories and retry"); + let roots = List.map (HExtlib.chop_prefix (Sys.getcwd()^"/")) roots in + prerr_endline ("Too many roots found:\n\t" ^ String.concat "\n\t" roots); + prerr_endline ("\nEnter one of these directories and retry"); exit 1 in let ma_files = args in -- 2.39.2