From f08e376eb0b370f92900182d3a5867a5b8c0cf7b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 14 Jul 2006 12:06:30 +0000 Subject: [PATCH] snapshot --- helm/www/matita/Makefile | 10 +++ helm/www/matita/images/folder-apache.png | Bin 0 -> 834 bytes helm/www/matita/images/matitina-apache.png | Bin 0 -> 590 bytes helm/www/matita/images/matitina-apache.svg | 65 ++++++++++++++++ helm/www/matita/images/matitina.svg | 63 ++++++++++++++++ helm/www/matita/matita.shtml | 83 ++++++++++----------- helm/www/matita/style.css | 9 ++- 7 files changed, 186 insertions(+), 44 deletions(-) create mode 100644 helm/www/matita/images/folder-apache.png create mode 100644 helm/www/matita/images/matitina-apache.png create mode 100644 helm/www/matita/images/matitina-apache.svg create mode 100644 helm/www/matita/images/matitina.svg diff --git a/helm/www/matita/Makefile b/helm/www/matita/Makefile index d31130452..6eb664099 100644 --- a/helm/www/matita/Makefile +++ b/helm/www/matita/Makefile @@ -15,6 +15,7 @@ all: @echo "Nothing to do per default, interesting targets:" @echo @echo " manual # import the (xhtml version of the) user manual" + @echo " library # import the scripts building the library" @echo " images # build images for the splash screen" @echo " papers # build the papers page from xml/papers.xml" @echo @@ -29,6 +30,15 @@ manual-stamp: $(DOCS_SRC_DIR)/*.xml $(DOCS_SRC_DIR)/xsl/* $(MAKE) -C $(DOCS_SRC_DIR) install DESTDIR=$(DOCS_DEST_DIR)/ touch $@ +.PHONY: library +library: + if [ -d library/ ] ; then \ + svn update library/ ; \ + else \ + echo "Can't find the scripts, check them out in library/" ; \ + exit 1 ; \ + fi + papers: papers.shtml papers.shtml: xsl/papers2xhtml.xsl xml/papers.xml xsltproc $^ > $@ diff --git a/helm/www/matita/images/folder-apache.png b/helm/www/matita/images/folder-apache.png new file mode 100644 index 0000000000000000000000000000000000000000..3a9b0bb105726920bdc909e3ebc3ffc22953869b GIT binary patch literal 834 zcmV-I1HJr-P)5}`Op8oeei}x1uz^Adm)6Y zA%v?Je0SLE^^PU!wZMbH;M!Z4*6yvZ4?jEqK?s4PqZi*cO}yvw{nr8mAKtw6{%>FI z?$Cq=$H8;p`SW9bc=$7q9zFRcHu0DL!Tc3?T6ZT@6)rIzkH8&wkUMp~!ks(Y^!xR0 z6XWhhG)qQ|iT!5>_h+-SFFLSHOireZMibn#;?P9?c=C+dG*H(o)T{M{GE+*dgoxyy z0AJP1LE~gH>#TVE_)j*jU1xji1M1Zplge$pTh*>+j3;CEo*r;^7U;l-hev#W{~^=q ztUG9HYnz>&PubXb8@Wi9kc3Qml`u2RjFck(9KGPdgC99Q9?ijU6iV*PAMynDdFc7&%sSI_qc3MW}P)l zmY9%Q8}eE%->ZQYpbzAdO0iR>ZgWvvJU98=qLgiEtto;Bby2<6DvmLB9xuZUnPbIw zEyT-U!ZeCfx{N0Tk?|p1G?+0FLyX|)EJI=3VG)?5-@57%$ zXg;riUh()A@J>l)wa}}1$@9zlx&Q5 z)Zc54aTv$(*S)9BY%&c|D>hb|O%(E@*pd^>?2xlL(2jPXlu$~MRt{t*N|7>@W%FZb zwiCs%a)L9-A0Q6Y4!#ba>(SG_=h-uN-F1Dg>(l%GUf=urezTMk$g->t*YE@L_=%a6 z(v+n>0UN|5no>%o+;aRze<@e%h0}O|dK|)SY>DDq+{5mr!akr5`=Y&s11R7*mSF-N zOM%TrFcqL%p*t`Uack6DYr$qB=)$&$J28uK9E@B$o}h6t*sENk2d}XX4bftE)OO-7 zvTCrec#k)j!xyY7Gpxi*w1qy3(Q2^Gm_{=)4B=|d)E1tW&}T5R02akvc#J~m3mDD; zyYUnap|4!~N2p#Z2y90E^-f&PQCpL+r_UPU1$y^?3KMqY9gN z5vR(I)H8JEJm+v0E%<}O6=7k%iQb6U#OAN9;F-h-E-wZv#5{F{-lTZ6$}fUmjG_@! zRbgc+H + + + + + + + + image/svg+xml + + + + + + + + + + diff --git a/helm/www/matita/images/matitina.svg b/helm/www/matita/images/matitina.svg new file mode 100644 index 000000000..76cdf9c2e --- /dev/null +++ b/helm/www/matita/images/matitina.svg @@ -0,0 +1,63 @@ + + + + + + + + + image/svg+xml + + + + + + + + + + diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml index ce58853f7..33a658479 100644 --- a/helm/www/matita/matita.shtml +++ b/helm/www/matita/matita.shtml @@ -14,31 +14,35 @@ Big Matita label -

Matita is a new document-centric interactive theorem prover that - integrates several Mathematical Knowledge - Management tools and techniques.

+

+ Matita (that means pencil in italian) is an experimental, + interactive theorem prover under development at the + Computer Science Department of the + University of Bologna. +

-

+ + +

Matita screenshot: authoring interface - Matita is traditional. Its logical foundation is the - Calculus of (Co)Inductive Constructions (CIC). It can re-use - mathematical concepts produced by other proof assistants (e.g. - Coq) when encoded in an - XML representation of CIC. The - interaction paradigm of Matita is familiar, being inspired by CtCoq and - Proof General. Its - proof language is procedural in the same spirit of LCF.

- -

Matita is innovative:

-
    - -
  • -

    - + + Matita is based on the + Calculus of (Co)Inductive Constructions, and is compatible, at some + extent, with Coq. + It is a reasonably small and simple application, whose + architectural and software complexity is meant to be mastered by + students, providing a tool particularly suited for testing innovative + ideas and solutions. + Matita adopts a tactic based editing mode; (XML-encoded) proof objects + are produced for storage and exchange. +

    + +

    + Matita screenshot: hyperlinks @@ -46,16 +50,14 @@ Matita screenshot: direct manipulation - the user interface sports high quality bidimensional rendering of - proofs and formulae transformed on-the-fly to MathML markup, on which direct - manipulation of the underlying CIC terms is still possible; -

    -
    • + The graphical interface has been inspired by CtCoq and + Proof General. + It supports high quality bidimensional rendering of + proofs and formulae transformed on-the-fly to + MathML markup

    -
  • -

    - +

    + Matita screenshot: library browsing @@ -64,31 +66,26 @@ - - the knowledge base is distributed: every authored concepts can be - published becoming part of the Matita library which can be browsed as an hypertext - (locally or on the World Wide Web) and searched by means of - content-based queries;

    -
    • + + + The knowledge base can be + browsed as an hypertext + (locally or on the World Wide Web) and + searched by means of + content-based queries;

    -
  • -

    +

    Matita screenshot: tinycals - the tactical language, part of the proof language, has + The tactical language, part of the proof language, has step-by-step semantics, enabling inspection and replaying of deeply structured proof scripts.

    -
    • - -
diff --git a/helm/www/matita/style.css b/helm/www/matita/style.css index c614becaa..d129be452 100644 --- a/helm/www/matita/style.css +++ b/helm/www/matita/style.css @@ -11,6 +11,7 @@ div.menu { left: 0px; width: 150px; text-align: center; + font-size: 10pt; } div.main { @@ -19,6 +20,7 @@ div.main { left: 150px; width: 650px; padding-left:20px; + font-size: 10pt; } div.news { @@ -81,6 +83,10 @@ ul { list-style-type: square; } +p.spaced { + padding-bottom: 2em; +} + /* menu */ div.menu ul { @@ -136,7 +142,8 @@ ul.wide li { div.topimage { text-align: left; - padding-top: 14px; + padding-top: 28px; + padding-bottom: 28px; } div.bottombar { -- 2.39.2