<head>
<title>Matita - Documentation</title>
<!--#include virtual="xhtml-meta.shtml" -->
+<script type="text/javascript">
+ function toggleAbstracts() {
+ abstracts = document.getElementsByTagName("span");
+ len = abstracts.length;
+ for (i=0; i != len-1; i++) {
+ elt = abstracts.item(i);
+ if (elt.hasAttribute("class")) {
+ if (elt.getAttribute("class") == "paper_abstract") {
+ if (elt.style.display != "none") {
+ elt.style.display = "none";
+ } else {
+ elt.style.display = "inline";
+ }
+ }
+ }
+ }
+ }
+</script>
</head>
<body>
<!--#include virtual="menubar.shtml" -->
available from our repository, in the
<a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk%2Fhelm%2Fsoftware%2Fmatita%2Fhelp%2FC%2F&rev=0&sc=0">matita/help/C/</a> folder. </p>
+ <h2>Tutorial<a name="tutorial"></a></h2>
+
+ <p>A not so short <a href="FILES/matita-tut.pdf">tutorial</a> by A.Asperti</p>
+
+ <h2>Exercises<a name="exercises"></a></h2>
+
+ <p>Some commented <a href="FILES/matita-ex.pdf">exercises</a> given at the
+ <a href="http://typessummerschool07.cs.unibo.it">types summer school 2007</a>
+ by C.Sacerdoti and E.Tassi.
+ </p>
<h2>Publications</h2>
<!--#include virtual="papers.shtml" -->
+ <h2>Large Developments</h2>
+ <!--#include virtual="theses.shtml" -->
+
<!--#include virtual="bottombar.shtml" -->
</div>
</body>
<h2>Releases<a name="releases"></a></h2>
<p>
- Matita has no official releases yet.
+ The current release (candidate) is version 0.4.98.
+ <dl>
+ <dt>Live CD</dt>
+
+ <dd>The <a href="FILES/matita-0.4.98-5.iso">live CD</a> (around 300
+ MB, md5sum: 2692090267bb551bb34d34ac189dafcf)
+ is the easiest way to try Matita. You can burn the CD image
+ and boot you computer from the CD, or install a free emulator like <a
+ href="http://virtualbox.org">virtualbox</a> and boot a virtual
+ machine from the CD image. Virtualbox is available for Mac OS X,
+ Windows and Linux.<br/>
+ </dd>
+
+ <dt>.deb package</dt>
+
+ <dd>Matita is part of the <a
+ href="http://packages.debian.org/source/matita"> Debian archive</a>, you can
+ install it with the following command:<pre>aptitude install matita matita-standard-library</pre>
+ Additionally it can be download adding the following line to your
+ <tt>/etc/apt/sources.list</tt> file: <pre>deb <a
+ href="http://mowgli.cs.unibo.it/~tassi/debian/">http://mowgli.cs.unibo.it/~tassi/debian/</a> ./ </pre>
+ </dd>
+
+ <dt>Sources</dt>
+
+ <dd>You can download the <a
+ href="FILES/matita_0.4.98.orig.tar.gz">sources</a> of Matita (around 2 MB, md5sum:
+ ef7449f06efc67d48ccbddbf55817ac3)
+ and
+ build it by yourself, following the <a
+ href="docs/manual/sec_install.html">installation instructions</a>.
+ The build process, due to the high number of external dependency is not
+ trivial, we thus suggest you to try the live CD or the .deb package
+ first.</dd>
+ </dl>
</p>
<h2>License<a name="license"></a></h2>
<p>
You can <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2F&sc=0">browse our svn repository</a> directly on the web.
</p>
+ <!-- THERE IS NO OPEN SVN SERVER ON MOWGLI
<p>
To checkout a copy of the sources type:
</p>
<a href="docs/manual/sec_install.html">installation instructions</a> on
how to build and install Matita from sources.
</p>
+ -->
<!--#include virtual="bottombar.shtml" -->
</div>
</body>
Matita can be <a href="library/">browsed on line</a>.
</p>
+ <br/>
+
+ <h1>Large Developments</h1>
+
+ <h2>Freescale<a name="freescale"></a></h2>
+ <p>
+ The <a href="freescale/">scripts</a> present:
+ </p>
+
+ <ul>
+ <li>an executable formalization of the operational semantics of
+ any <a href="http://www.freescale.com">Freescale</a>
+ micro-controller of the <a href="http://www.freescale.com/webapp/sps/site/homepage.jsp?nodeId=0162468449&tid=FSH">HC05/HC08/RS08/HCS08 families</a>
+ <li>a compiler from assembly language (pseudocodes + operands) to
+ machine code
+ <li>several automatic checks for unhandled opcodes, memory accesses,
+ correctness of ALU logic, etc.
+ <li>three examples of assembly programs (string reverse, counting sort
+ and perfect numbers sieve) with sets of data to run them
+ </ul>
+ </a>
+
+ <p>The execution in the executable formalization has been compared
+ to real world execution using the <a href="http://www.freescale.com/webapp/sps/site/overview.jsp?code=784_LPBBNEWTOOL&fsrch=1">USB SPYDER08</a>
+ in-circuit debugger.
+ </p>
+
+ <p>
+ The code (in <a href="http://caml.inria.fr">OCaml</a>)
+ of an executable <a href="freescale/freescale_ocaml">emulator</a>,
+ automatically generated from the scripts above. On the tests above,
+ it runs at about 29% of the speed of the
+ <a href="http://www.freescale.com/codewarrior">CodeWarrior</a>
+ emulation engine.
+ </p>
+
+ <p>The formalization has been the Undergraduate Thesis of
+ Mr. Cosimo Oliboni. The manuscript (italian only) can be found
+ <a href="http://matita.cs.unibo.it/documentation.shtml#freescale">
+ here</a>.
+ </p>
+
<!--#include virtual="bottombar.shtml" -->
</div>
</body>
-<!-- $Id$ -->
<!--#include virtual="xhtml-header.shtml" -->
-<html>
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta name="keywords" content="Matita, prover, assistant" />
<title>Matita - Home Page</title>
step-by-step semantics, enabling inspection and replaying of deeply
structured proof scripts. </p>
- <p>Matita is partially supported by the following Projects:
+ <p>Matita is partially supported by the following Projects: </p>
<ul>
- <li><a href=http://www.cs.chalmers.se/Cs/Research/Logic/Types/>
- Types Project</a>
- <li><a href=http://www.mctafi.math.unipd.it/>McTafi</a></li>
- <li><a href=http://dama.cs.unibo.it/>Dama</a></li>
+ <li><a href="http://www.cs.chalmers.se/Cs/Research/Logic/Types/">
+ Types Project</a></li>
+ <li><a href="http://www.mctafi.math.unipd.it/">McTafi</a></li>
+ <li><a href="http://dama.cs.unibo.it/">Dama</a></li>
</ul>
- </p>
<!--#include virtual="bottombar.shtml" -->
</div>
<!-- $Id$ -->
<div class="news">
- <strong>News:</strong>
- <ul>
+ <div class="newsheader">News</div>
+ <ul class="news">
+ <li><span class="date">18 Dec 2007</span><br />
+ Matita release candidate 0.4.98 available for <a href="download.shtml">download</a>.
+ </li>
+ <li><span class="date">18 Dec 2007</span><br />
+ Added a tutorial and some exercises to the <a href="documentation.shtml">documentation</a>
+ page.
+ </li>
<li><span class="date">20 Mar 2007</span><br />
A course on Matita at the
<a href="http://typessummerschool07.cs.unibo.it">Types Summer School 2007</a>.
-<script type="text/javascript">
- function toggleAbstracts() {
- abstracts = document.getElementsByTagName("span");
- len = abstracts.length;
- for (i=0; i != len-1; i++) {
- elt = abstracts.item(i);
- if (elt.hasAttribute("class")) {
- if (elt.getAttribute("class") == "paper_abstract") {
- if (elt.style.display != "none") {
- elt.style.display = "none";
- } else {
- elt.style.display = "inline";
- }
- }
- }
- }
- }
-</script>
<small>
<a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
</small>
font-weight: bold;
}
+dt {
+ margin-top:1em;
+ font-weight: bold;
+}
+
+ul.news li {
+ margin-bottom: 1em;
+ list-style-type: none;
+}
+
+ul.news li span.date {
+ font-weight: bold;
+}
+
+div.news div.newsheader {
+ text-align: center;
+ margin-left:auto;
+ margin-right:auto;
+ font-weight: bold;
+}
-<!-- $Id$ -->
<?xml version="1.0" encoding="UTF-8" ?>
+<!-- $Id$ -->
<?xml-stylesheet type="text/css" href="style.css" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
projects / helm.git / commitdiff