From 9d356a6f202a77fb1dd67b57b1c86ac3ebe1382b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 30 Apr 2008 10:46:54 +0000
Subject: [PATCH] many pending modifications were there, now the website at
least validates
---
helm/www/matita/documentation.shtml | 31 +++++++++++++++++++++
helm/www/matita/download.shtml | 38 +++++++++++++++++++++++++-
helm/www/matita/library.shtml | 42 +++++++++++++++++++++++++++++
helm/www/matita/matita.shtml | 15 +++++------
helm/www/matita/news.shtml | 11 ++++++--
helm/www/matita/papers.shtml | 18 -------------
helm/www/matita/style.css | 20 ++++++++++++++
helm/www/matita/xhtml-header.shtml | 2 +-
8 files changed, 147 insertions(+), 30 deletions(-)
diff --git a/helm/www/matita/documentation.shtml b/helm/www/matita/documentation.shtml
index 3fb209455..0e8f63ae4 100644
--- a/helm/www/matita/documentation.shtml
+++ b/helm/www/matita/documentation.shtml
@@ -4,6 +4,24 @@
Matita - Documentation
+
@@ -30,10 +48,23 @@
available from our repository, in the
matita/help/C/ folder.
+ Tutorial
+
+ A not so short tutorial by A.Asperti
+
+ Exercises
+
+ Some commented exercises given at the
+ types summer school 2007
+ by C.Sacerdoti and E.Tassi.
+
Publications
+ Large Developments
+
+
diff --git a/helm/www/matita/download.shtml b/helm/www/matita/download.shtml
index 1c07e00b2..45fd3e4aa 100644
--- a/helm/www/matita/download.shtml
+++ b/helm/www/matita/download.shtml
@@ -12,7 +12,41 @@
Releases
- Matita has no official releases yet.
+ The current release (candidate) is version 0.4.98.
+
+ - Live CD
+
+ - The live CD (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 virtualbox and boot a virtual
+ machine from the CD image. Virtualbox is available for Mac OS X,
+ Windows and Linux.
+
+
+ - .deb package
+
+ - Matita is part of the Debian archive, you can
+ install it with the following command:
aptitude install matita matita-standard-library
+ Additionally it can be download adding the following line to your
+ /etc/apt/sources.list file: deb http://mowgli.cs.unibo.it/~tassi/debian/ ./
+
+
+ - Sources
+
+ - You can download the sources of Matita (around 2 MB, md5sum:
+ ef7449f06efc67d48ccbddbf55817ac3)
+ and
+ build it by yourself, following the installation instructions.
+ 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.
+
License
@@ -27,6 +61,7 @@
You can browse our svn repository directly on the web.
+
diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml
index 6617949a5..a6f195b63 100644
--- a/helm/www/matita/library.shtml
+++ b/helm/www/matita/library.shtml
@@ -16,6 +16,48 @@
Matita can be browsed on line.
+
+
+ Large Developments
+
+ Freescale
+
+ The scripts present:
+
+
+
+ - an executable formalization of the operational semantics of
+ any Freescale
+ micro-controller of the HC05/HC08/RS08/HCS08 families
+
- a compiler from assembly language (pseudocodes + operands) to
+ machine code
+
- several automatic checks for unhandled opcodes, memory accesses,
+ correctness of ALU logic, etc.
+
- three examples of assembly programs (string reverse, counting sort
+ and perfect numbers sieve) with sets of data to run them
+
+
+
+ The execution in the executable formalization has been compared
+ to real world execution using the USB SPYDER08
+ in-circuit debugger.
+
+
+
+ The code (in OCaml)
+ of an executable emulator,
+ automatically generated from the scripts above. On the tests above,
+ it runs at about 29% of the speed of the
+ CodeWarrior
+ emulation engine.
+
+
+ The formalization has been the Undergraduate Thesis of
+ Mr. Cosimo Oliboni. The manuscript (italian only) can be found
+
+ here.
+
+
diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 845367ad1..4c9e166c5 100644
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -1,6 +1,6 @@
-
-
+
+
Matita - Home Page
@@ -91,14 +91,13 @@
step-by-step semantics, enabling inspection and replaying of deeply
structured proof scripts.
- Matita is partially supported by the following Projects:
+
Matita is partially supported by the following Projects:
-
diff --git a/helm/www/matita/news.shtml b/helm/www/matita/news.shtml
index 306a6d17a..6aec5d333 100644
--- a/helm/www/matita/news.shtml
+++ b/helm/www/matita/news.shtml
@@ -1,8 +1,15 @@
-
News:
-
+
+
+ - 18 Dec 2007
+ Matita release candidate 0.4.98 available for download.
+
+ - 18 Dec 2007
+ Added a tutorial and some exercises to the documentation
+ page.
+
- 20 Mar 2007
A course on Matita at the
Types Summer School 2007.
diff --git a/helm/www/matita/papers.shtml b/helm/www/matita/papers.shtml
index 2e67afd9a..886a87271 100644
--- a/helm/www/matita/papers.shtml
+++ b/helm/www/matita/papers.shtml
@@ -1,21 +1,3 @@
-
[ Toggle abstracts ]
diff --git a/helm/www/matita/style.css b/helm/www/matita/style.css
index 38abf1714..a34f0a5aa 100644
--- a/helm/www/matita/style.css
+++ b/helm/www/matita/style.css
@@ -223,3 +223,23 @@ span.paper_title {
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;
+}
diff --git a/helm/www/matita/xhtml-header.shtml b/helm/www/matita/xhtml-header.shtml
index ad156d651..3bfa720fb 100644
--- a/helm/www/matita/xhtml-header.shtml
+++ b/helm/www/matita/xhtml-header.shtml
@@ -1,5 +1,5 @@
-
+
--
2.39.2