@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
$(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 $^ > $@
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://web.resource.org/cc/"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ width="744.09448819"
+ height="1052.3622047"
+ id="svg1879"
+ sodipodi:version="0.32"
+ inkscape:version="0.44"
+ sodipodi:docbase="/home/zack"
+ sodipodi:docname="matitina-apache.svg">
+ <defs
+ id="defs1881" />
+ <sodipodi:namedview
+ id="base"
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1.0"
+ gridtolerance="10000"
+ guidetolerance="10"
+ objecttolerance="10"
+ inkscape:pageopacity="0.0"
+ inkscape:pageshadow="2"
+ inkscape:zoom="14.738889"
+ inkscape:cx="385.71429"
+ inkscape:cy="652.82322"
+ inkscape:document-units="px"
+ inkscape:current-layer="layer1"
+ inkscape:window-width="902"
+ inkscape:window-height="579"
+ inkscape:window-x="10"
+ inkscape:window-y="71" />
+ <metadata
+ id="metadata1884">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <g
+ inkscape:label="Layer 1"
+ inkscape:groupmode="layer"
+ id="layer1">
+ <g
+ transform="matrix(0.957434,0.288652,-0.288652,0.957434,376.8964,394.9313)"
+ style="fill:black;fill-rule:evenodd;stroke:none;stroke-width:0pt;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none"
+ id="g4"
+ inkscape:export-xdpi="260.08759"
+ inkscape:export-ydpi="260.08759">
+ <path
+ d="M 1.586,0.867 C 1.265,0.867 0.867,1.375 0.867,1.793 C 0.867,1.985 1.007,2.153 1.175,2.153 C 1.484,2.153 1.863,1.645 1.863,1.227 C 1.863,1.028 1.746,0.867 1.586,0.867 z M 2.293,0 C 2.293,0 0.808,0.25 0.808,0.25 C 0.808,0.25 0,1.606 0,1.606 C 0,1.606 0.41,3.141 0.41,3.141 C 0.41,3.141 4.734,5.739 4.734,5.739 C 4.871,5.821 5.082,5.879 5.261,5.879 C 5.261,5.879 8.019,5.879 8.019,5.879 C 8.261,5.879 8.379,5.801 8.379,5.641 C 8.379,5.578 8.371,5.551 8.308,5.442 C 8.308,5.442 6.886,2.942 6.886,2.942 C 6.777,2.742 6.726,2.692 6.566,2.602 C 6.566,2.602 6.464,2.543 6.464,2.543 C 6.464,2.543 2.293,0 2.293,0 z M 2.211,0.239 C 2.211,0.239 2.55,1.426 2.55,1.426 C 2.55,1.426 1.824,2.66 1.824,2.66 C 1.824,2.66 0.617,2.918 0.617,2.918 C 0.617,2.918 0.289,1.625 0.289,1.625 C 0.289,1.625 0.976,0.469 0.976,0.469 C 0.976,0.469 2.211,0.239 2.211,0.239 z M 7.562,4.614 C 7.781,4.942 7.781,4.953 7.781,5.043 C 7.781,5.16 7.632,5.41 7.504,5.532 C 7.433,5.602 7.293,5.641 7.144,5.641 C 7.144,5.641 5.34,5.641 5.34,5.641 C 6.277,5.012 6.675,4.325 6.754,3.239 C 6.754,3.239 7.562,4.614 7.562,4.614 z M 2.543,0.418 C 2.543,0.418 6.464,2.809 6.464,2.809 C 6.496,2.989 6.507,3.078 6.507,3.207 C 6.507,3.348 6.496,3.449 6.464,3.649 C 6.464,3.649 2.82,1.465 2.82,1.465 C 2.82,1.465 2.543,0.418 2.543,0.418 z M 2.699,1.664 C 2.699,1.664 6.379,3.887 6.379,3.887 C 6.336,4.157 5.98,4.754 5.75,4.934 C 5.75,4.934 2.074,2.699 2.074,2.699 C 2.074,2.699 2.699,1.664 2.699,1.664 z M 1.953,2.91 C 1.953,2.91 5.59,5.102 5.59,5.102 C 5.429,5.289 5.101,5.578 4.972,5.641 C 4.972,5.641 0.847,3.117 0.847,3.117 C 0.847,3.117 1.953,2.91 1.953,2.91 z "
+ id="path6" />
+ </g>
+ </g>
+</svg>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://web.resource.org/cc/"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ width="744.09448819"
+ height="1052.3622047"
+ id="svg1879"
+ sodipodi:version="0.32"
+ inkscape:version="0.44"
+ sodipodi:docbase="/home/zack"
+ sodipodi:docname="matitina.svg">
+ <defs
+ id="defs1881" />
+ <sodipodi:namedview
+ id="base"
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1.0"
+ gridtolerance="10000"
+ guidetolerance="10"
+ objecttolerance="10"
+ inkscape:pageopacity="0.0"
+ inkscape:pageshadow="2"
+ inkscape:zoom="14.738889"
+ inkscape:cx="385.71429"
+ inkscape:cy="652.85714"
+ inkscape:document-units="px"
+ inkscape:current-layer="layer1"
+ inkscape:window-width="902"
+ inkscape:window-height="579"
+ inkscape:window-x="10"
+ inkscape:window-y="71" />
+ <metadata
+ id="metadata1884">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <g
+ inkscape:label="Layer 1"
+ inkscape:groupmode="layer"
+ id="layer1">
+ <g
+ transform="translate(378.6676,403.7084)"
+ style="fill:black;fill-rule:evenodd;stroke:none;stroke-width:0pt;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none"
+ id="g4">
+ <path
+ d="M 1.586,0.867 C 1.265,0.867 0.867,1.375 0.867,1.793 C 0.867,1.985 1.007,2.153 1.175,2.153 C 1.484,2.153 1.863,1.645 1.863,1.227 C 1.863,1.028 1.746,0.867 1.586,0.867 z M 2.293,0 C 2.293,0 0.808,0.25 0.808,0.25 C 0.808,0.25 0,1.606 0,1.606 C 0,1.606 0.41,3.141 0.41,3.141 C 0.41,3.141 4.734,5.739 4.734,5.739 C 4.871,5.821 5.082,5.879 5.261,5.879 C 5.261,5.879 8.019,5.879 8.019,5.879 C 8.261,5.879 8.379,5.801 8.379,5.641 C 8.379,5.578 8.371,5.551 8.308,5.442 C 8.308,5.442 6.886,2.942 6.886,2.942 C 6.777,2.742 6.726,2.692 6.566,2.602 C 6.566,2.602 6.464,2.543 6.464,2.543 C 6.464,2.543 2.293,0 2.293,0 z M 2.211,0.239 C 2.211,0.239 2.55,1.426 2.55,1.426 C 2.55,1.426 1.824,2.66 1.824,2.66 C 1.824,2.66 0.617,2.918 0.617,2.918 C 0.617,2.918 0.289,1.625 0.289,1.625 C 0.289,1.625 0.976,0.469 0.976,0.469 C 0.976,0.469 2.211,0.239 2.211,0.239 z M 7.562,4.614 C 7.781,4.942 7.781,4.953 7.781,5.043 C 7.781,5.16 7.632,5.41 7.504,5.532 C 7.433,5.602 7.293,5.641 7.144,5.641 C 7.144,5.641 5.34,5.641 5.34,5.641 C 6.277,5.012 6.675,4.325 6.754,3.239 C 6.754,3.239 7.562,4.614 7.562,4.614 z M 2.543,0.418 C 2.543,0.418 6.464,2.809 6.464,2.809 C 6.496,2.989 6.507,3.078 6.507,3.207 C 6.507,3.348 6.496,3.449 6.464,3.649 C 6.464,3.649 2.82,1.465 2.82,1.465 C 2.82,1.465 2.543,0.418 2.543,0.418 z M 2.699,1.664 C 2.699,1.664 6.379,3.887 6.379,3.887 C 6.336,4.157 5.98,4.754 5.75,4.934 C 5.75,4.934 2.074,2.699 2.074,2.699 C 2.074,2.699 2.699,1.664 2.699,1.664 z M 1.953,2.91 C 1.953,2.91 5.59,5.102 5.59,5.102 C 5.429,5.289 5.101,5.578 4.972,5.641 C 4.972,5.641 0.847,3.117 0.847,3.117 C 0.847,3.117 1.953,2.91 1.953,2.91 z "
+ id="path6" />
+ </g>
+ </g>
+</svg>
<img src="images/matita-text-big.png" alt="Big Matita label" />
</div>
- <p> Matita is a new document-centric interactive theorem prover that
- integrates several <a href="http://www.mkm-ig.org">Mathematical Knowledge
- Management</a> tools and techniques. </p>
+ <p class="spaced">
+ Matita (that means <em>pencil</em> in italian) is an experimental,
+ interactive theorem prover under development at the
+ <a href="http://www.cs.unibo.it">Computer Science Department</a> of the
+ <a href="http://www.unibo.it">University of Bologna</a>.
+ </p>
- <p>
+<!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
+
+ <p class="spaced">
<span class="screenshots">
<a class="quiet" href="images/screenshot-matita.png">
<img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
</a>
</span>
- Matita is <strong>traditional</strong>. Its logical foundation is the
- Calculus of (Co)Inductive Constructions (CIC). It can re-use
- mathematical concepts produced by other proof assistants (e.g.
- <a href="http://coq.inria.fr">Coq</a>) when encoded in an
- <a href="http://www.w3.org/XML/">XML</a> representation of CIC. The
- interaction paradigm of Matita is familiar, being inspired by CtCoq and
- <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>. Its
- proof language is procedural in the same spirit of LCF. </p>
-
- <p> Matita is <strong>innovative</strong>: </p>
- <ul>
-
- <li>
- <p>
- <span class="screenshots">
+
+ Matita is based on the
+ Calculus of (Co)Inductive Constructions, and is compatible, at some
+ extent, with <a href="http://coq.inria.fr">Coq</a>.
+ 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.
+ </p>
+
+ <p class="spaced">
+ <span class="screenshots">
<a class="quiet" href="images/screenshot-matita-href.png">
<img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
</a>
<img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
</a>
</span>
- the user interface sports high quality bidimensional rendering of
- proofs and formulae transformed on-the-fly to <a
- href="http://www.w3.org/Math/">MathML</a> markup, on which direct
- manipulation of the underlying CIC terms is still possible;
- </p>
- </li>
+ The graphical interface has been inspired by CtCoq and
+ <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
+ It supports high quality bidimensional rendering of
+ proofs and formulae transformed on-the-fly to
+ <a href="http://www.w3.org/Math/">MathML</a> markup</p>
- <li>
- <p>
- <span class="screenshots">
+ <p class="spaced">
+ <span class="screenshots">
<a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
<img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
</a>
</a>
<!--
<a class="quiet" href="images/screenshot-cicbrowser-proof.png">
- <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering" />
+ <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
</a>
-->
- </span>
- the knowledge base is distributed: every authored concepts can be
- published becoming part of the Matita library which can be <a
- href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
- (locally or on the World Wide Web) and <a
- href="http://helm.cs.unibo.it/whelp/"> searched by means of
- content-based queries</a>; </p>
- </li>
+ </span>
+
+ The knowledge base can be
+ <a href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
+ (locally or on the World Wide Web) and
+ <a href="http://helm.cs.unibo.it/whelp/"> searched by means of
+ content-based queries</a>; </p>
- <li>
- <p>
+ <p class="spaced">
<span class="screenshots">
<a class="quiet" href="images/screenshot-tinycals.png">
<img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
</a>
</span>
- 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. </p>
- </li>
-
- </ul>
<!--#include virtual="bottombar.shtml" -->
</div>
left: 0px;
width: 150px;
text-align: center;
+ font-size: 10pt;
}
div.main {
left: 150px;
width: 650px;
padding-left:20px;
+ font-size: 10pt;
}
div.news {
list-style-type: square;
}
+p.spaced {
+ padding-bottom: 2em;
+}
+
/* menu */
div.menu ul {
div.topimage {
text-align: left;
- padding-top: 14px;
+ padding-top: 28px;
+ padding-bottom: 28px;
}
div.bottombar {
projects / helm.git / commitdiff
