From: Andrea Asperti Date: Tue, 3 Apr 2012 07:46:45 +0000 (+0000) Subject: Created a new directory for Matita1.0 X-Git-Tag: make_still_working~1829 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fcaa64e1cf492478f5d93ca041d6d18d6b4faf9d;p=helm.git Created a new directory for Matita1.0 --- diff --git a/helm/www/matita1.0/.htaccess b/helm/www/matita1.0/.htaccess new file mode 100644 index 000000000..ed0105bf0 --- /dev/null +++ b/helm/www/matita1.0/.htaccess @@ -0,0 +1,3 @@ + + Deny from all + diff --git a/helm/www/matita1.0/CLUSTERCS/Makefile b/helm/www/matita1.0/CLUSTERCS/Makefile new file mode 100644 index 000000000..21723aa96 --- /dev/null +++ b/helm/www/matita1.0/CLUSTERCS/Makefile @@ -0,0 +1,3 @@ +all: + dpkg-scanpackages -m . /dev/null | gzip > Packages.gz + dpkg-scansources . /dev/null | gzip > Sources.gz diff --git a/helm/www/matita1.0/DEBIAN/Makefile b/helm/www/matita1.0/DEBIAN/Makefile new file mode 100644 index 000000000..21723aa96 --- /dev/null +++ b/helm/www/matita1.0/DEBIAN/Makefile @@ -0,0 +1,3 @@ +all: + dpkg-scanpackages -m . /dev/null | gzip > Packages.gz + dpkg-scansources . /dev/null | gzip > Sources.gz diff --git a/helm/www/matita1.0/FILES/matita-ex.pdf b/helm/www/matita1.0/FILES/matita-ex.pdf new file mode 100644 index 000000000..eb73f6c72 Binary files /dev/null and b/helm/www/matita1.0/FILES/matita-ex.pdf differ diff --git a/helm/www/matita1.0/FILES/matita-tut.pdf b/helm/www/matita1.0/FILES/matita-tut.pdf new file mode 100644 index 000000000..17003d36b Binary files /dev/null and b/helm/www/matita1.0/FILES/matita-tut.pdf differ diff --git a/helm/www/matita1.0/FILES/matita_0.5.0.orig.tar.gz b/helm/www/matita1.0/FILES/matita_0.5.0.orig.tar.gz new file mode 100644 index 000000000..4bec5293f Binary files /dev/null and b/helm/www/matita1.0/FILES/matita_0.5.0.orig.tar.gz differ diff --git a/helm/www/matita1.0/FILES/matita_0.5.1.orig.tar.gz b/helm/www/matita1.0/FILES/matita_0.5.1.orig.tar.gz new file mode 100644 index 000000000..cd99b804b Binary files /dev/null and b/helm/www/matita1.0/FILES/matita_0.5.1.orig.tar.gz differ diff --git a/helm/www/matita1.0/FILES/matita_0.5.2.orig.tar.gz b/helm/www/matita1.0/FILES/matita_0.5.2.orig.tar.gz new file mode 100644 index 000000000..2f4ec448c Binary files /dev/null and b/helm/www/matita1.0/FILES/matita_0.5.2.orig.tar.gz differ diff --git a/helm/www/matita1.0/FILES/matita_0.5.3.orig.tar.gz b/helm/www/matita1.0/FILES/matita_0.5.3.orig.tar.gz new file mode 100644 index 000000000..241cbb344 Binary files /dev/null and b/helm/www/matita1.0/FILES/matita_0.5.3.orig.tar.gz differ diff --git a/helm/www/matita1.0/FILES/matita_0.5.4.orig.tar.gz b/helm/www/matita1.0/FILES/matita_0.5.4.orig.tar.gz new file mode 100644 index 000000000..4faac3d3b Binary files /dev/null and b/helm/www/matita1.0/FILES/matita_0.5.4.orig.tar.gz differ diff --git a/helm/www/matita1.0/FILES/matita_0.5.5.orig.tar.gz b/helm/www/matita1.0/FILES/matita_0.5.5.orig.tar.gz new file mode 100644 index 000000000..666ce5b35 Binary files /dev/null and b/helm/www/matita1.0/FILES/matita_0.5.5.orig.tar.gz differ diff --git a/helm/www/matita1.0/FILES/matita_0.5.6.orig.tar.gz b/helm/www/matita1.0/FILES/matita_0.5.6.orig.tar.gz new file mode 100644 index 000000000..94d753fbf Binary files /dev/null and b/helm/www/matita1.0/FILES/matita_0.5.6.orig.tar.gz differ diff --git a/helm/www/matita1.0/FILES/matita_0.5.7.orig.tar.gz b/helm/www/matita1.0/FILES/matita_0.5.7.orig.tar.gz new file mode 100644 index 000000000..e2818daa3 Binary files /dev/null and b/helm/www/matita1.0/FILES/matita_0.5.7.orig.tar.gz differ diff --git a/helm/www/matita1.0/Makefile b/helm/www/matita1.0/Makefile new file mode 100644 index 000000000..c54475713 --- /dev/null +++ b/helm/www/matita1.0/Makefile @@ -0,0 +1,78 @@ + +# should be a checked out version of sofware/matita/help/C/ (or a symlink to it) +DOCS_SRC_DIR = docs-src +DOCS_DEST_DIR = $(CURDIR)/docs/manual +# should be a checked out and compiled with -execcomments of +# sofware/matita/nlibrary/topology/igft.ma +TUTORIAL_SRC_DIR = tutorial-src +TUTORIAL_DEST_DIR = $(CURDIR)/docs/tutorial + +MARGIN_X=30 +MARGIN_Y=206 +SIZE_X=426 +SIZE_Y=70 + +SEQ=3 + +all: + @echo + @echo "Nothing to do per default, interesting targets:" + @echo + @echo " manual # import the (xhtml version of the) user manual" + @echo " tutorial # import the html version of the topology tutorial" + @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 + +clean: + +manual: manual-stamp +manual-stamp: $(DOCS_SRC_DIR)/*.xml $(DOCS_SRC_DIR)/xsl/* + $(MAKE) -C $(DOCS_SRC_DIR)/ html + rm -rf $(DOCS_DEST_DIR)/* + test -d $(DOCS_DEST_DIR)/ || mkdir -p $(DOCS_DEST_DIR)/ + $(MAKE) -C $(DOCS_SRC_DIR) install-html DESTDIR=$(DOCS_DEST_DIR)/ + touch $@ + +tutorial: tutorial-stamp +tutorial-stamp: $(TUTORIAL_SRC_DIR)/igft.html + rm -rf $(TUTORIAL_DEST_DIR)/* + test -d $(TUTORIAL_DEST_DIR)/ || mkdir -p $(TUTORIAL_DEST_DIR)/ + cp $(TUTORIAL_SRC_DIR)/igft.html $(TUTORIAL_DEST_DIR)/ + cp $(TUTORIAL_SRC_DIR)/igft.pdf $(TUTORIAL_DEST_DIR)/ + cp $(TUTORIAL_SRC_DIR)/*.png $(TUTORIAL_DEST_DIR)/ + cp $(TUTORIAL_SRC_DIR)/*.svg $(TUTORIAL_DEST_DIR)/ + cp $(TUTORIAL_SRC_DIR)/*.css $(TUTORIAL_DEST_DIR)/ + cp $(TUTORIAL_SRC_DIR)/*.js $(TUTORIAL_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 $^ > $@ + +.PHONY: images +images: images/matita.xcf + for Y in `seq 0 $(SEQ)`; do \ + convert images/matita.png -crop \ + $(SIZE_X)x$(SIZE_Y)+$(MARGIN_X)+`expr $(MARGIN_Y) + $$Y '*' '(' $(SIZE_Y) + 1 ')'` tmp.png; \ + composite -compose src-over images/bg.png tmp.png images/bg$$Y.png;\ + done;\ + rm tmp.png + +clean: + rm -f manual-stamp +dist-clean: clean + for X in `seq 0 $(SEQ)`; do\ + rm images/bg$$X.png;\ + done + diff --git a/helm/www/matita1.0/PAPERS/disambiguation-errors.pdf b/helm/www/matita1.0/PAPERS/disambiguation-errors.pdf new file mode 100644 index 000000000..5dec013e3 Binary files /dev/null and b/helm/www/matita1.0/PAPERS/disambiguation-errors.pdf differ diff --git a/helm/www/matita1.0/PAPERS/disambiguation.pdf b/helm/www/matita1.0/PAPERS/disambiguation.pdf new file mode 100644 index 000000000..664204d70 Binary files /dev/null and b/helm/www/matita1.0/PAPERS/disambiguation.pdf differ diff --git a/helm/www/matita1.0/PAPERS/hopr.pdf b/helm/www/matita1.0/PAPERS/hopr.pdf new file mode 100644 index 000000000..40fb659a1 Binary files /dev/null and b/helm/www/matita1.0/PAPERS/hopr.pdf differ diff --git a/helm/www/matita1.0/PAPERS/matita.pdf b/helm/www/matita1.0/PAPERS/matita.pdf new file mode 100644 index 000000000..ef1e3bd38 Binary files /dev/null and b/helm/www/matita1.0/PAPERS/matita.pdf differ diff --git a/helm/www/matita1.0/PAPERS/matita_types.pdf b/helm/www/matita1.0/PAPERS/matita_types.pdf new file mode 100644 index 000000000..20c3e544a Binary files /dev/null and b/helm/www/matita1.0/PAPERS/matita_types.pdf differ diff --git a/helm/www/matita1.0/PAPERS/notation.pdf b/helm/www/matita1.0/PAPERS/notation.pdf new file mode 100644 index 000000000..07cd63a18 Binary files /dev/null and b/helm/www/matita1.0/PAPERS/notation.pdf differ diff --git a/helm/www/matita1.0/PAPERS/oliboni.pdf b/helm/www/matita1.0/PAPERS/oliboni.pdf new file mode 100644 index 000000000..c65f859e5 Binary files /dev/null and b/helm/www/matita1.0/PAPERS/oliboni.pdf differ diff --git a/helm/www/matita1.0/PAPERS/tinycals.pdf b/helm/www/matita1.0/PAPERS/tinycals.pdf new file mode 100644 index 000000000..c4c86931e Binary files /dev/null and b/helm/www/matita1.0/PAPERS/tinycals.pdf differ diff --git a/helm/www/matita1.0/PAPERS/whelp.pdf b/helm/www/matita1.0/PAPERS/whelp.pdf new file mode 100644 index 000000000..b9a7294a2 Binary files /dev/null and b/helm/www/matita1.0/PAPERS/whelp.pdf differ diff --git a/helm/www/matita1.0/UBUNTU_HARDY/Makefile b/helm/www/matita1.0/UBUNTU_HARDY/Makefile new file mode 100644 index 000000000..21723aa96 --- /dev/null +++ b/helm/www/matita1.0/UBUNTU_HARDY/Makefile @@ -0,0 +1,3 @@ +all: + dpkg-scanpackages -m . /dev/null | gzip > Packages.gz + dpkg-scansources . /dev/null | gzip > Sources.gz diff --git a/helm/www/matita1.0/UBUNTU_INTREPID/Makefile b/helm/www/matita1.0/UBUNTU_INTREPID/Makefile new file mode 100644 index 000000000..21723aa96 --- /dev/null +++ b/helm/www/matita1.0/UBUNTU_INTREPID/Makefile @@ -0,0 +1,3 @@ +all: + dpkg-scanpackages -m . /dev/null | gzip > Packages.gz + dpkg-scansources . /dev/null | gzip > Sources.gz diff --git a/helm/www/matita1.0/bottombar.shtml b/helm/www/matita1.0/bottombar.shtml new file mode 100644 index 000000000..6c480c44a --- /dev/null +++ b/helm/www/matita1.0/bottombar.shtml @@ -0,0 +1,11 @@ + +

+ Last-modified: +

+ +

diff --git a/helm/www/matita1.0/bugzilla.css b/helm/www/matita1.0/bugzilla.css new file mode 100644 index 000000000..5638fb0d3 --- /dev/null +++ b/helm/www/matita1.0/bugzilla.css @@ -0,0 +1,11 @@ +div#page-index .intro +{ + width: 225px; + height: 225px; + + margin-top: 2.3em; + margin-right: 2.3em; + float: right; + + background: transparent no-repeat url(http://matita.cs.unibo.it/images/matita-medium.png); +} diff --git a/helm/www/matita1.0/cgi-bin/hl.cgi b/helm/www/matita1.0/cgi-bin/hl.cgi new file mode 100755 index 000000000..f2a146ccc --- /dev/null +++ b/helm/www/matita1.0/cgi-bin/hl.cgi @@ -0,0 +1,84 @@ +#!/usr/bin/perl -w +use strict; + +# Copyright (C) 2006, HELM Team. +# +# This file is part of HELM, an Hypertextual, Electronic +# Library of Mathematics, developed at the Computer Science +# Department, University of Bologna, Italy. +# +# HELM is free software; you can redistribute it and/or +# modify it under the terms of the GNU General Public License +# as published by the Free Software Foundation; either version 2 +# of the License, or (at your option) any later version. +# +# HELM is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with HELM; if not, write to the Free Software +# Foundation, Inc., 59 Temple Place - Suite 330, Boston, +# MA 02111-1307, USA. +# +# For details, see the HELM World-Wide-Web page, +# http://helm.cs.unibo.it/ + +use CGI; +use Syntax::Highlight::Universal; + +# Configuration + +my $documentroot = '/projects/matita/public_html/'; +my $protohrc = $documentroot . 'helm-proto.hrc'; +my $scriptsdir = $documentroot . 'library/'; + +my %formatmap = ( + '.ma' => 'grafite', + '.c' => 'c', # debug +); + +# Code + +my $query = CGI->new; # used globally by some 'sub' below +print $query->header(-type=>'text/html', -charset=>'utf-8'); + +sub die_invalid_file() { + print $query->start_html; + print 'Invalid script.'; + print $query->end_html; + exit 0; +} + +sub lookup_script($) { + my ($f) = @_; + die_invalid_file() unless $f =~ /^(.*)(\.[^.]+)$/; + my $base = $1; + my $extension = $2; + die_invalid_file() unless $base =~ /[-a-zA-Z_]+(\/[-a-zA-Z_])*/; + die_invalid_file() unless exists $formatmap{$extension}; + my $path = $scriptsdir . $f; + die_invalid_file() unless -f $path; + return ($path, $formatmap{$extension}); +} + +my $fname = $query->param('f'); + +my $highlighter = Syntax::Highlight::Universal->new; +$highlighter->addConfig($protohrc); + +my ($script, $format) = lookup_script($fname); +open SCRIPT, "< $script" or die "Can't open Matita script \"$script\"\n"; +my @lines = + + + +

Matita Documentation

+ +

User Manual

+ +

The Matita User Manual is accessible from Matita itself via the + GNOME Help + System, just hit <F1> while running Matita and it + will be shown to you.

+ +

Alternatively you can browse it in + XHTML format: +

Matita User Manual (XHTML format, multiple pages) +

+ +

The source code of the user manual (in DocBook format) is + available from our repository, in the + matita/help/C/ folder.

+ +

Tutorials

+ +

A not so short tutorial by + A.Asperti, discussing some basic notions of number theory, for + the stable version of Matita.

+ +

A tutorial by E.Tassi based on + the formalization of the paper "Between formal topology and game theory: + an explicit solution for the conditions for an inductive generation of + formal topologies" by S.Berardi and S.Valentini. The tutorial describes + the ng version of Matita (not officially released yet, cohexisting with + the stable system in version 0.5.8). If some characters are not displayed + correctly (i.e. you are not using firefox) you may try the + pdf version. +

+ + +

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/matita1.0/download.shtml b/helm/www/matita1.0/download.shtml new file mode 100644 index 000000000..737ee6379 --- /dev/null +++ b/helm/www/matita1.0/download.shtml @@ -0,0 +1,102 @@ + + + + + Matita - Download + + + + +

Download Matita!

+ +

Releases

+ The current version is 0.5.8, released on January 8, 2010. Here the + ChangeLog. +

Live CD

The live CD (around 530 + MB, md5sum: +9a6912765eacaaa7f96d7d6d6b34add5 + ) + 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. A short guide to VirtualBox is part of the + Matita manual
+

.deb package

Matita is part of the Debian archive, you can + install it with the following command:

aptitude install matita

Sources

You can download the sources of Matita (around 6 MB, md5sum: +125223d3dc522c4ac063a66f5d46df69 + ) + 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

+ All our source code is released under the terms of the GNU General Public + Licence and is publically accessible on our Subversion repository. +

+ +

Subversion repository

+ You can browse our svn repository directly on the web. +

+ +

Nightly builds

+ A build of the Debian package is performed every night, and a live CD containing that version is also built. + You can download this experimental live CD, or add the Debian repository + to your apt configuration file: +

+      deb http://matita.cs.unibo.it/DEBIAN ./
+      deb-src http://matita.cs.unibo.it/DEBIAN ./
+

+ +

Cluster .cs.unibo.it.

+ The following repository contains the version of Matita installed + in the Ercolani laboratory, currently running Ubuntu Jaunty. +

+      deb http://matita.cs.unibo.it/CLUSTERCS ./
+      deb-src http://matita.cs.unibo.it/CLUSTERCS ./
+

+ The same version is also available for Ubuntu Hardy (LTS) +

+      deb http://matita.cs.unibo.it/UBUNTU_HARDY ./
+      deb-src http://matita.cs.unibo.it/UBUNTU_HARDY ./
+

+ + + +

+ + diff --git a/helm/www/matita1.0/flags/wgb.gif b/helm/www/matita1.0/flags/wgb.gif new file mode 100644 index 000000000..9d6edc452 Binary files /dev/null and b/helm/www/matita1.0/flags/wgb.gif differ diff --git a/helm/www/matita1.0/flags/wit.gif b/helm/www/matita1.0/flags/wit.gif new file mode 100644 index 000000000..1009b5270 Binary files /dev/null and b/helm/www/matita1.0/flags/wit.gif differ diff --git a/helm/www/matita1.0/grafite-format.css b/helm/www/matita1.0/grafite-format.css new file mode 100644 index 000000000..cb902f503 --- /dev/null +++ b/helm/www/matita1.0/grafite-format.css @@ -0,0 +1,85 @@ +/* color scheme similar to the colors we use in gtksourceview */ + +.grafite_TheoremKinds { + color: #a52a2a; + font-weight: bold; +} + +.grafite_Commands { + color: #a52a2a; + font-weight: bold; +} + +.grafite_Tactics { + color: #008b8b; + /*font-style: italic;*/ +} + +.grafite_Macros { + color: #a020f0; +} + +.grafite_Sorts { + color: #2e8b57; +} + +.grafite_Operators { + color: #a020f0; +} + +.grafite_String { + color: #ff00ff; +} + +.grafite_Comment { + color: #0000ff; +} + +.grafite_Symbols { + color: #a52a2a; + font-weight: bold; +} + +/* color scheme from colorer's navy.css stylesheet */ + +/* +.grafite_TheoremKinds { + color: #7779bb; + font-weight: bold; +} + +.grafite_Commands { + color: #200080; + font-weight: bold; +} + +.grafite_Tactics { + color: #930000; + font-style: italic; +} + +.grafite_Macros { + color: #004a43; +} + +.grafite_Sorts { + color: #7779bb; +} + +.grafite_Operators { + color: #44aadd; +} + +.grafite_String { + color: #1060b6; +} + +.grafite_Comment { + color: #595979; +} + +.grafite_Symbols { + color: #406080; + font-weight: bold; +} +*/ diff --git a/helm/www/matita1.0/grafite.hrc b/helm/www/matita1.0/grafite.hrc new file mode 100644 index 000000000..7ebf82f63 --- /dev/null +++ b/helm/www/matita1.0/grafite.hrc @@ -0,0 +1,179 @@ + + + + + + + + + Grafite: Matita scripts language + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/www/matita1.0/helm-proto.hrc b/helm/www/matita1.0/helm-proto.hrc new file mode 100644 index 000000000..90b623542 --- /dev/null +++ b/helm/www/matita1.0/helm-proto.hrc @@ -0,0 +1,24 @@ + + + + + + + This is a base HRC file with prototype defines and types linking information. + + + + + + + /\.ma$/i + + + + + + + diff --git a/helm/www/matita1.0/images/MINI_screenshot-cicbrowser-browsing.png b/helm/www/matita1.0/images/MINI_screenshot-cicbrowser-browsing.png new file mode 100644 index 000000000..e5c1d5575 Binary files /dev/null and b/helm/www/matita1.0/images/MINI_screenshot-cicbrowser-browsing.png differ diff --git a/helm/www/matita1.0/images/MINI_screenshot-cicbrowser-proof.png b/helm/www/matita1.0/images/MINI_screenshot-cicbrowser-proof.png new file mode 100644 index 000000000..469fbb984 Binary files /dev/null and b/helm/www/matita1.0/images/MINI_screenshot-cicbrowser-proof.png differ diff --git a/helm/www/matita1.0/images/MINI_screenshot-cicbrowser-query.png b/helm/www/matita1.0/images/MINI_screenshot-cicbrowser-query.png new file mode 100644 index 000000000..08c052532 Binary files /dev/null and b/helm/www/matita1.0/images/MINI_screenshot-cicbrowser-query.png differ diff --git a/helm/www/matita1.0/images/MINI_screenshot-matita-href.png b/helm/www/matita1.0/images/MINI_screenshot-matita-href.png new file mode 100644 index 000000000..22b878cbc Binary files /dev/null and b/helm/www/matita1.0/images/MINI_screenshot-matita-href.png differ diff --git a/helm/www/matita1.0/images/MINI_screenshot-matita-selection.png b/helm/www/matita1.0/images/MINI_screenshot-matita-selection.png new file mode 100644 index 000000000..66a045a28 Binary files /dev/null and b/helm/www/matita1.0/images/MINI_screenshot-matita-selection.png differ diff --git a/helm/www/matita1.0/images/MINI_screenshot-matita.png b/helm/www/matita1.0/images/MINI_screenshot-matita.png new file mode 100644 index 000000000..5296d0faf Binary files /dev/null and b/helm/www/matita1.0/images/MINI_screenshot-matita.png differ diff --git a/helm/www/matita1.0/images/MINI_screenshot-tinycals.png b/helm/www/matita1.0/images/MINI_screenshot-tinycals.png new file mode 100644 index 000000000..c6a9491e8 Binary files /dev/null and b/helm/www/matita1.0/images/MINI_screenshot-tinycals.png differ diff --git a/helm/www/matita1.0/images/README.minis b/helm/www/matita1.0/images/README.minis new file mode 100644 index 000000000..05d555206 --- /dev/null +++ b/helm/www/matita1.0/images/README.minis @@ -0,0 +1,4 @@ +To generate miniatures: + + for f in screenshot-* ; do convert -resize 100 $f MINI_$f ; done + diff --git a/helm/www/matita1.0/images/bg.png b/helm/www/matita1.0/images/bg.png new file mode 100644 index 000000000..a3d5532d4 Binary files /dev/null and b/helm/www/matita1.0/images/bg.png differ diff --git a/helm/www/matita1.0/images/bg0.png b/helm/www/matita1.0/images/bg0.png new file mode 100644 index 000000000..fc751234d Binary files /dev/null and b/helm/www/matita1.0/images/bg0.png differ diff --git a/helm/www/matita1.0/images/bg1.png b/helm/www/matita1.0/images/bg1.png new file mode 100644 index 000000000..f2aa2ce59 Binary files /dev/null and b/helm/www/matita1.0/images/bg1.png differ diff --git a/helm/www/matita1.0/images/bg2.png b/helm/www/matita1.0/images/bg2.png new file mode 100644 index 000000000..42538230e Binary files /dev/null and b/helm/www/matita1.0/images/bg2.png differ diff --git a/helm/www/matita1.0/images/bg3.png b/helm/www/matita1.0/images/bg3.png new file mode 100644 index 000000000..081b149d5 Binary files /dev/null and b/helm/www/matita1.0/images/bg3.png differ diff --git a/helm/www/matita1.0/images/folder-apache.png b/helm/www/matita1.0/images/folder-apache.png new file mode 100644 index 000000000..3a9b0bb10 Binary files /dev/null and b/helm/www/matita1.0/images/folder-apache.png differ diff --git a/helm/www/matita1.0/images/matita-library.png b/helm/www/matita1.0/images/matita-library.png new file mode 100644 index 000000000..0add006f6 Binary files /dev/null and b/helm/www/matita1.0/images/matita-library.png differ diff --git a/helm/www/matita1.0/images/matita-medium.png b/helm/www/matita1.0/images/matita-medium.png new file mode 100644 index 000000000..b91dfa986 Binary files /dev/null and b/helm/www/matita1.0/images/matita-medium.png differ diff --git a/helm/www/matita1.0/images/matita-small.png b/helm/www/matita1.0/images/matita-small.png new file mode 100644 index 000000000..15b5ac691 Binary files /dev/null and b/helm/www/matita1.0/images/matita-small.png differ diff --git a/helm/www/matita1.0/images/matita-text-big.png b/helm/www/matita1.0/images/matita-text-big.png new file mode 100644 index 000000000..b76d87446 Binary files /dev/null and b/helm/www/matita1.0/images/matita-text-big.png differ diff --git a/helm/www/matita1.0/images/matita-tiny.png b/helm/www/matita1.0/images/matita-tiny.png new file mode 100644 index 000000000..b67a5b533 Binary files /dev/null and b/helm/www/matita1.0/images/matita-tiny.png differ diff --git a/helm/www/matita1.0/images/matita-w-text-big.png b/helm/www/matita1.0/images/matita-w-text-big.png new file mode 100644 index 000000000..f7e8a5e07 Binary files /dev/null and b/helm/www/matita1.0/images/matita-w-text-big.png differ diff --git a/helm/www/matita1.0/images/matita-w-text-small.png b/helm/www/matita1.0/images/matita-w-text-small.png new file mode 100644 index 000000000..f6a234f2a Binary files /dev/null and b/helm/www/matita1.0/images/matita-w-text-small.png differ diff --git a/helm/www/matita1.0/images/matita.png b/helm/www/matita1.0/images/matita.png new file mode 100644 index 000000000..7ef6f4b9b Binary files /dev/null and b/helm/www/matita1.0/images/matita.png differ diff --git a/helm/www/matita1.0/images/matita.xcf b/helm/www/matita1.0/images/matita.xcf new file mode 100644 index 000000000..d4b1804fa Binary files /dev/null and b/helm/www/matita1.0/images/matita.xcf differ diff --git a/helm/www/matita1.0/images/matitina-apache.png b/helm/www/matita1.0/images/matitina-apache.png new file mode 100644 index 000000000..a1f50fa56 Binary files /dev/null and b/helm/www/matita1.0/images/matitina-apache.png differ diff --git a/helm/www/matita1.0/images/matitina-apache.svg b/helm/www/matita1.0/images/matitina-apache.svg new file mode 100644 index 000000000..b586e6379 --- /dev/null +++ b/helm/www/matita1.0/images/matitina-apache.svg @@ -0,0 +1,65 @@ + + + diff --git a/helm/www/matita1.0/images/matitina.svg b/helm/www/matita1.0/images/matitina.svg new file mode 100644 index 000000000..76cdf9c2e --- /dev/null +++ b/helm/www/matita1.0/images/matitina.svg @@ -0,0 +1,63 @@ + + + diff --git a/helm/www/matita1.0/images/screenshot-cicbrowser-browsing.png b/helm/www/matita1.0/images/screenshot-cicbrowser-browsing.png new file mode 100644 index 000000000..76bb4822e Binary files /dev/null and b/helm/www/matita1.0/images/screenshot-cicbrowser-browsing.png differ diff --git a/helm/www/matita1.0/images/screenshot-cicbrowser-proof.png b/helm/www/matita1.0/images/screenshot-cicbrowser-proof.png new file mode 100644 index 000000000..f52bc6ea6 Binary files /dev/null and b/helm/www/matita1.0/images/screenshot-cicbrowser-proof.png differ diff --git a/helm/www/matita1.0/images/screenshot-cicbrowser-query.png b/helm/www/matita1.0/images/screenshot-cicbrowser-query.png new file mode 100644 index 000000000..c19c38221 Binary files /dev/null and b/helm/www/matita1.0/images/screenshot-cicbrowser-query.png differ diff --git a/helm/www/matita1.0/images/screenshot-matita-href.png b/helm/www/matita1.0/images/screenshot-matita-href.png new file mode 100644 index 000000000..699d1e14a Binary files /dev/null and b/helm/www/matita1.0/images/screenshot-matita-href.png differ diff --git a/helm/www/matita1.0/images/screenshot-matita-selection.png b/helm/www/matita1.0/images/screenshot-matita-selection.png new file mode 100644 index 000000000..5c85bd357 Binary files /dev/null and b/helm/www/matita1.0/images/screenshot-matita-selection.png differ diff --git a/helm/www/matita1.0/images/screenshot-matita.png b/helm/www/matita1.0/images/screenshot-matita.png new file mode 100644 index 000000000..b72080b45 Binary files /dev/null and b/helm/www/matita1.0/images/screenshot-matita.png differ diff --git a/helm/www/matita1.0/images/screenshot-tinycals.png b/helm/www/matita1.0/images/screenshot-tinycals.png new file mode 100644 index 000000000..c64612ecd Binary files /dev/null and b/helm/www/matita1.0/images/screenshot-tinycals.png differ diff --git a/helm/www/matita1.0/images/sheetbg.png b/helm/www/matita1.0/images/sheetbg.png new file mode 100644 index 000000000..3583db8db Binary files /dev/null and b/helm/www/matita1.0/images/sheetbg.png differ diff --git a/helm/www/matita1.0/images/valid-css.png b/helm/www/matita1.0/images/valid-css.png new file mode 100644 index 000000000..9b2f596e0 Binary files /dev/null and b/helm/www/matita1.0/images/valid-css.png differ diff --git a/helm/www/matita1.0/images/valid-xhtml10.png b/helm/www/matita1.0/images/valid-xhtml10.png new file mode 100644 index 000000000..2275ee6ea Binary files /dev/null and b/helm/www/matita1.0/images/valid-xhtml10.png differ diff --git a/helm/www/matita1.0/index.shtml b/helm/www/matita1.0/index.shtml new file mode 120000 index 000000000..2fad15b04 --- /dev/null +++ b/helm/www/matita1.0/index.shtml @@ -0,0 +1 @@ +matita.shtml \ No newline at end of file diff --git a/helm/www/matita1.0/library.shtml b/helm/www/matita1.0/library.shtml new file mode 100644 index 000000000..c42fa673b --- /dev/null +++ b/helm/www/matita1.0/library.shtml @@ -0,0 +1,199 @@ + + + + + Matita - Library + + + + +

Matita Library

+ +

Scripts

+ The scripts used to generate the knowledge base of + Matita can be browsed on line. +

+ The experimental scripts for the next major version of Matita can also be browsed on line. +

+ +
+ +

Large Developments

+ +

Certified Complexity (CerCo)

Matita is being used to certify a cost preserving compiler from a + large subset of C into the 8051 machine code. The compiler does not + only produce the target code, but it also instruments the source code + with precise cost declarations for the execution of O(1) code + fragments. This induced cost model for the source language is + inherently non compositional since it is affected by the compilation + strategy: the same instructions are compiled in different ways in + different contexts, yielding different costs. +

The final aim of the CerCo project is to formally reason on + intensional properties on the C code -- e.g. to show that some hard + deadline is always met + -- and to be sure that the property holds also for the target code. +

The CerCo project is a FET Open IST project funded by the EU + community in the 7th Framework Programme. More informations on the + project and the code of the Matita formalization can be found + on the CerCo Web site +

+ +

The Basic Picture

+ The scripts present a formalization + of some results from the forthcoming book The Basic Picture - Structures for Constructive Topology by Giovanni Sambin. +

The formalization has been the result of a three years long + collaboration between mathematicians from the University of Padova + and computer scientists from the University of + Bologna, funded by the University of Padova. In particular, + the groups that collaborated are headed respectively by Prof. Sambin + in Padua (formal topology and constructive type theory) + and by Prof. Asperti in Bologna (constructive type theory and interactive + theorem proving). +

+ In particular the scripts present: +

the category of Basic Pairs, that are generalizations of + topological spaces
the category of Basic Topologies, that are generalizations of + formal topologies
the existence of a categorical embedding of the former category + into the latter. The embedding is an improvement on the usual + adjunction between topological spaces and locales

+ All the results are presented constructively and in the predicative + fragment of Matita based on the minimalist type theory + by Maietti and Sambin, where choice axioms are not valid. +

+ In order to reason comfortably on the previous concrete categories and + functors, we also present algebraic versions of all the introduced + notions, as well as categorical embedding of the concrete categories in + the algebrized ones. In particular we formalized: +

the large category of Overlap Algebras, that extends locales with an + axiomatized (= algebraized) overlap binary predicate. The + concrete overlap predicate states positively + (i.e. without using negation) the existence (in the intuitionistic + sense) of a point in the intersection of two sets. + Morphisms of Overlap Algebras algebrize concrete relations between + sets by means of four functions that capture the + existential and universal pre and post images of a relation. +
the large category of O-Basic Pairs, that algebraize Basic + Pairs by means of Overlap Algebras
the large category of O-Basic Topologies, that algebraize Basic + Topologies by means of Overlap Algebras
the categorical embedding of Basic Pairs into O-Basic Pairs and + of Basic Topologies into O-Basic Topologies
the existence of a categorical embedding of the category + of O-Basic Pairs into the category of O-Basic Topologies

+ More information will be available in a forthcoming paper by + Claudio Sacerdoti Coen and Enrico Tassi to be + published in the Mathematical Structures in Computer Science journal. +

+ +

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. +

+ +

The Formal System λδ (lambda_delta)

+ +

The formal system λδ is a typed λ-calculus that + pursues the unification of terms, types, environments and contexts + as the main goal. + λδ takes some features from the Automath-related + λ-calculi and some from the pure type systems, but differs + from both in that it does not include the Π construction while it + provides for an abbreviation mechanism at the level of terms. +

+ +

The development presents the proofs of some important properties that + λδ enjoys. In particular: +

the confluence of reduction
the correctness of types
the uniqueness of types up to conversion
the subject reduction of the type assignment
the strong normalization of the typed terms
the decidability of type inference problem

+ +

+ See the λδ home page + for more information. +

+ +

Small Developments

+ +

Pointed regular expressions

+ The script present: +

+ +

a formalization of the syntax and semantics of pointed regular + expressions, that are regular expressions where points are put + in front of atoms to describe where the next character recognized + by the expression should be. Multiple points represent the union + of multiple languages. A pointed regular expression corresponds + to a state of a regular automaton for the regular expression + obtained erasing all points.
a formalization of the construction of the automaton for a regular + expression by means of iterative computation of pointed regular + expressions.
a proof of correctness of the construction (to be completed)

+ +

The development requires the SVN version of Matita to be executed.

+ + +

+ + diff --git a/helm/www/matita1.0/matita.shtml b/helm/www/matita1.0/matita.shtml new file mode 100644 index 000000000..4c9e166c5 --- /dev/null +++ b/helm/www/matita1.0/matita.shtml @@ -0,0 +1,105 @@ + + + + + + Matita - Home Page + + + + + +

+ +

+ 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 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. +

+ +

+ + + + + + + + + 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

+ +

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

+ +

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

+ +

Matita is partially supported by the following Projects:

+ + +

+ + diff --git a/helm/www/matita1.0/matita_it.shtml b/helm/www/matita1.0/matita_it.shtml new file mode 100644 index 000000000..eeafd975e --- /dev/null +++ b/helm/www/matita1.0/matita_it.shtml @@ -0,0 +1,110 @@ + + + + + + Matita - Home Page Italiana + + + + + +

+ +

+ Matita e' un tool sperimentale di supporto alla dimostrazione + interattiva di teoremi, in via di sviluppo al + Dipartimento di Scienze + dell'Informazione della + Universita' degli Studi di Bologna. +

+ + + +

+ + + + + + + Matita e' basato sul Calcolo delle Costruzioni (Co)Induttive, ed + parzialmente compatibile con l'analogo strumento francese + Coq. + Matita e' una applicazione ragionevolmente semplice e piccola, + la cui complessita' architetturale puo' essere + padroneggiata da laureandi, facendone uno strumento particolarmente + utile per la sperimentazione di nuove idee e soluzioni in ambito + universitario. + Matita adotta una filosofia di scrittura delle prove basata su + tattiche; lambda-termini di prova (codificati in XML) sono prodotti + per la memorizzazione di lungo periodo e lo scambio di dati + con altri sistemi. +

+ +

+ + + + + + + + + L'interfaccia grafica e' stata ispirata da CtCoq e + Proof General. + Supporta una resa bidimensionale di alta qualita' delle espressioni + basata sul markup + MathML.

+ +

+ + + + + + + + + + + La base di conoscenza matematica puo' + essere + visitata come un ipertesto + (localmente o sul World Wide Web) e si possono effettuare + ricerche basate su + interrogazioni contenutistiche;

+ +

+ + + + + + Il linguaggio delle tattiche, parte del vernacolo di prova, + ha una semantica passo-passo che consente di ispezionare e + eseguire in modo non atomico anche scripts altamente strutturati.

+ +

Matita e' finanziato parzialmente dai seguenti progetti: +

+ +

+ + diff --git a/helm/www/matita1.0/menubar.shtml b/helm/www/matita1.0/menubar.shtml new file mode 100644 index 000000000..3c06e1836 --- /dev/null +++ b/helm/www/matita1.0/menubar.shtml @@ -0,0 +1,21 @@ + + + + diff --git a/helm/www/matita1.0/menubar_it.shtml b/helm/www/matita1.0/menubar_it.shtml new file mode 100644 index 000000000..732e1e466 --- /dev/null +++ b/helm/www/matita1.0/menubar_it.shtml @@ -0,0 +1,21 @@ + + + + diff --git a/helm/www/matita1.0/navy.css b/helm/www/matita1.0/navy.css new file mode 100644 index 000000000..335b37276 --- /dev/null +++ b/helm/www/matita1.0/navy.css @@ -0,0 +1,247 @@ +/* Generated with hrd2css.pl from ./Colorer-take5.beta4/hrd/rgb/navy.hrd */ + +.def_HorzCross { + color: #000000; + background-color: #e8e7f8; +} + +.def_VertCross { + color: #000000; + background-color: #e1e0f2; +} + +.def_Number { + color: #008c00; +} + +.def_NumberDec { + color: #008c00; +} + +.def_NumberHex { + color: #008000; +} + +.def_NumberBin { + color: #005b00; +} + +.def_NumberOct { + color: #008c00; +} + +.def_NumberFloat { + color: #008000; +} + +.def_NumberSuffix { + color: #006600; +} + +.def_String { + color: #1060b6; +} + +.def_StringContent { + color: #0f69ff; +} + +.def_StringEdge { + color: #800000; +} + +.def_CharacterContent { + color: #0000cc; +} + +.def_Comment { + color: #595979; +} + +.def_CommentContent { + color: #7F9FBF; + font-weight: bold; +} + +.def_CommentEdge { + color: #606090; +} + +.def_CommentDoc { + color: #3F7F8F; +} + +.def_CommentDocEdge { + color: #c0bd92; +} + +.def_Symbol { + color: #308080; +} + +.def_SymbolStrong { + color: #406080; +} + +.def_Prefix { + color: #0066ee; +} + +.def_Operator { + color: #44aadd; +} + +.def_Keyword { + color: #200080; + font-weight: bold; +} + +.def_KeywordStrong { + color: #7779bb; + font-weight: bold; +} + +.def_FunctionKeyword { + color: #400000; +} + +.def_DeprecatedKeyword { + color: #008484; +} + +.def_InterfaceKeyword { + color: #008484; +} + +.def_ClassKeyword { + color: #6679aa; + font-weight: bold; +} + +.def_StructKeyword { + color: #003060; +} + +.def_TypeKeyword { + color: #7779bb; +} + +.def_Register { + color: #000080; +} + +.def_Constant { + color: #7d0045; +} + +.def_Var { + color: #007d45; +} + +.def_VarStrong { + color: #007997; +} + +.def_Identifier { + color: #005fd2; +} + +.def_BooleanConstant { + color: #0f4d75; +} + +.def_Directive { + color: #004a43; +} + +.def_Parameter { + color: #074726; +} + +.def_ParameterUnknown { + color: #474796; +} + +.def_Tag { + color: #333385; +} + +.def_OpenTag { + color: #0057a6; +} + +.def_CloseTag { + color: #0057a6; +} + +.def_Label { + color: #e34adc; +} + +.def_LabelStrong { + color: #000000; + background-color: #a8a800; +} + +.def_Insertion { + color: #000000; + background-color: #cceeee; +} + +.def_Error { + color: #ffffff; + background-color: #dd9999; + font-weight: bold; + font-style: italic; +} + +.def_ErrorText { + color: #ee00ee; +} + +.def_TODO { + color: #ffffff; + background-color: #808000; +} + +.def_Debug { + color: #80abfd; + background-color: #007084; +} + +.def_Path { + color: #40015a; +} + +.def_URL { + color: #5555DD; +} + +.def_EMail { + color: #7144c4; +} + +.def_Date { + color: #009797; +} + +.def_Time { + color: #8745a0; +} + +.def_PairStart { + color: #d0d0ff; +} + +.def_PairEnd { + color: #d0d0ff; +} + +.def_PairStrongStart { + color: #880088; +} + +.def_PairStrongEnd { + color: #880088; +} + diff --git a/helm/www/matita1.0/news.shtml b/helm/www/matita1.0/news.shtml new file mode 100644 index 000000000..7c448cf6c --- /dev/null +++ b/helm/www/matita1.0/news.shtml @@ -0,0 +1,65 @@ + + +

News

8 January 2010
+ Matita release 0.5.8 available for download. +
7 August 2009
+ Matita-prover scores best new entry at the + CADE ATP System Competition (UEQ). +
15 February 2009
+ Matita release 0.5.7 available for download. +
1 December 2008
+ Matita release 0.5.6 available for download. +
17 November 2008
+ Matita release 0.5.5 available for download. +
19 October 2008
+ Matita release 0.5.4 available for download. +
23 July 2008
+ Matita release 0.5.3 available for download. +
2 July 2008
+ Matita release 0.5.2 available for download. +
10 May 2008
+ Matita release 0.5.0 available for download. +
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. +
24 Jan 2007
+ Solution for the Poplmark challenge (part 1a) +
1 Dic 2006
+ + Presentation of Matita to the Italian Association for + Mathematics. +
21 Aug 2006
+ Matita-prover on TPTP. +
18 Jul 2006
+ the scripts of the library are now + on-line +
14 Jun 2006
+ mailing lists for Matita are now + available +

+ diff --git a/helm/www/matita1.0/news_it.shtml b/helm/www/matita1.0/news_it.shtml new file mode 120000 index 000000000..33f473db9 --- /dev/null +++ b/helm/www/matita1.0/news_it.shtml @@ -0,0 +1 @@ +news.shtml \ No newline at end of file diff --git a/helm/www/matita1.0/papers.shtml b/helm/www/matita1.0/papers.shtml new file mode 100644 index 000000000..886a87271 --- /dev/null +++ b/helm/www/matita1.0/papers.shtml @@ -0,0 +1,239 @@ + + [ Toggle abstracts ] + + +

+ + Andrea Asperti, Enrico Tassi +
+ + Higher order proof reconstruction from paramodulation-based refutations: + the unit equality case + + + .pdf + + + Accepted for publication in the proceedings of MKM 2007: The 6th + International Conference on Mathematical Knowledge Management. + + + In this paper we address the problem of reconstructing a + higher order, checkable proof object starting from a proof trace left by a + first order automatic proof searching procedure, in a restricted equational + framework. The automatic procedure is based on superposition rules for + the unit equality case. Proof transformation techniques aimed to improve + the readability of the final proof are discussed. + +
+ + Claudio Sacerdoti Coen, Stefano Zacchiroli +
+ + Spurious Disambiguation Error Detection + + + .pdf + + + Accepted for publication in the proceedings of MKM 2007: The 6th + International Conference on Mathematical Knowledge Management. + + + The disambiguation approach to the input of formulae enables the user to + type correct formulae in a terse syntax close to the usual ambiguous + mathematical notation. When it comes to incorrect formulae we want to + present only errors related to the interpretation meant by the user, hiding + errors related to other interpretations (spurious errors). We propose a + heuristic to recognize spurious errors, which has been integrated with our + former efficient disambiguation algorithm. + +
+ + Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli +
+ + Crafting a Proof Assistant + + + .pdf + + + Accepted for publication in the Proceedings of Types 2006: Conference of + the Types Project. Nottingham, UK -- April 18-21, 2006. + + + Proof assistants are complex applications whose develop- + ment has never been properly systematized or documented. This work is + a contribution in this direction, based on our experience with the devel- + opment of Matita: a new interactive theorem prover basedâas Coqâon + the Calculus of Inductive Constructions (CIC). In particular, we analyze + its architecture focusing on the dependencies of its components, how they + implement the main functionalities, and their degree of reusability. + The work is a first attempt to provide a ground for a more direct com- + parison between different systems and to highlight the common func- + tionalities, not only in view of reusability but also to encourage a more + systematic comparison of different softwares and architectural solutions. + +
+ + Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli +
+ + User Interaction with the Matita Proof Assistant + + + .pdf + + + Accepted for publication in Journal of Automated Reasoning, Special Issue + on User Interfaces for Theorem Proving. + + + Matita is a new, document-centric, tactic-based interactive theorem + prover. This paper focuses on some of the distinctive features of the user interaction + with Matita, mostly characterized by the organization of the library as a search- + able knowledge base, the emphasis on a high-quality notational rendering, and the + complex interplay between syntax, presentation, and semantics. + +
+ + Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli +
+ + Tinycals: step by step tacticals + + + .pdf + + + In Proceedings of UITP 2006: User Interfaces for Theorem Provers. Seattle, + WA -- August 21, 2006. ENTCS, Volume 174, Issue 2 (May 2007), Pages 125 - + 142, ISSN:1571-0661 + + + Most of the state-of-the-art proof assistants are based on procedural + proof languages, scripts, and rely on LCF tacticals as the primary tool + for tactics composition. In this paper we discuss how these ingredients + do not interact well with user interfaces based on the same interaction + paradigm of Proof General (the de facto standard in this field), + identifying in the coarse-grainedness of tactical evaluation the key + problem. + + We propose tinycals as an alternative to a subset of LCF tacticals, + showing that the user does not experience the same problem if tacticals + are evaluated in a more fine-grained manner. We present the formal + operational semantics of tinycals as well as their implementation in the + Matita proof assistant. + +
+ Luca Padovani, Stefano Zacchiroli
+ + From notation to semantics: there and back again + + + .pdf + + + Accepted for publication in the proceedings of MKM 2006: The 5th + International Conference on Mathematical Knowledge Management. + Wokingham, UK -- August 11-12, 2006. + + + Mathematical notation is a structured, open, and ambiguous language. In + order to support mathematical notation in MKM applications one must + necessarily take into account presentational as well as semantic aspects. + The former are required to create a familiar, comfortable, and usable + interface to interact with. The latter are necessary in order to process + the information meaningfully. In this paper we investigate a framework + for dealing with mathematical notation in a meaningful, extensible way, + and we show an effective instantiation of its architecture to the field + of interactive theorem proving. The framework builds upon well-known + concepts and widely-used technologies and it can be easily adopted by + other MKM applications. + +
+ + Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli +
+ + A content based mathematical search engine: Whelp + + + .pdf + + + In Proceedings of TYPES 2004 conference Types for Proofs and Programs. + Paris, France -- December 15-18, 2004. LNCS 3839/2004, Springer-Verlag + Heidelberg, ISBN 3-540-31428-8, pp. 17-32 + + + The prototype of a content based search engine for mathematical knowledge + supporting a small set of queries requiring matching and/or typing + operations is described. The prototype, called Whelp, exploits a metadata + approach for indexing the information that looks far more flexible than + traditional indexing techniques for structured expressions like + substitution, discrimination, or context trees. The prototype has been + instantiated to the standard library of the Coq proof assistant extended + with many user contributions. + +
+ + Claudio Sacerdoti Coen, Stefano Zacchiroli +
+ + Efficient Ambiguous Parsing of Mathematical Formulae + + + .pdf + + + In Proceedings of MKM 2004 + Third International Conference on Mathematical Knowledge Management. + September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004, + Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362 + + + Mathematical notation has the characteristic of being ambiguous: + operators can be overloaded and information that can be deduced is often + omitted. Mathematicians are used to this ambiguity and can easily + disambiguate a formula making use of the context and of their ability to + find the right interpretation. + + Software applications that have to deal with formulae usually avoid these + issues by fixing an unambiguous input notation. This solution is annoying + for mathematicians because of the resulting tricky syntaxes and becomes a + show stopper to the simultaneous adoption of tools characterized by + different input languages. + + In this paper we present an efficient algorithm suitable for ambiguous + parsing of mathematical formulae. The only requirement of the algorithm + is the existence of a validity predicate over abstract syntax trees of + incomplete formulae with placeholders. This requirement can be easily + fulfilled in the applicative area of interactive proof assistants, and in + several other areas of Mathematical Knowledge Management. + +

diff --git a/helm/www/matita1.0/splash.shtml b/helm/www/matita1.0/splash.shtml new file mode 100644 index 000000000..0d45599c3 --- /dev/null +++ b/helm/www/matita1.0/splash.shtml @@ -0,0 +1,66 @@ + + + + + Matita - Splash + + + + + +

+ +

1. Developers
2. Documentation
3. Community
4. Download

+ + + diff --git a/helm/www/matita1.0/style.css b/helm/www/matita1.0/style.css new file mode 100644 index 000000000..00eef2ed1 --- /dev/null +++ b/helm/www/matita1.0/style.css @@ -0,0 +1,248 @@ +/* + * CSS stylesheet for the website http://matita.cs.unibo.it/ + * + * $Id$ + */ + +/* page layout */ + +div.menu { + position: absolute; + left: 0px; + width: 150px; + text-align: center; + font-size: 10pt; +} + +div.main { + position: absolute; + top: 0px; + left: 150px; + width: 650px; + padding-left:20px; + font-size: 10pt; +} + +div.news { + position: absolute; + top: 25px; + left: 845px; + font-size: 10pt; + width: 150px; + background: #eaeaea; + padding: 5px; + display: block; + height: 90%; + overflow: hidden; +} + +/* site-wide typesetting */ + +body { + font-family: sans-serif; + font-size: 12pt; + background-image: url(images/sheetbg.png); + background-repeat: repeat; +} + +h1 { + font-size: 18pt; + color: #808080; + + text-align: center; +} + +h2 { + font-size: 16pt; + color: #808080; + + border-bottom-style: solid; + border-width: 3px; + border-color: #cb8080; +} + +h3 { + font-size: 14pt; + color: #808080; +} + +h4 { + font-size: 13pt; + color: #808080; +} + +a { + margin: 2px; + color: #591622; + text-decoration: underline; +} + +a:hover { + text-decoration: underline; + background-color: #ecf6f9; +} + +ul { + list-style-type: square; +} + +p.spaced { + padding-bottom: 2em; +} + +/* menu */ + +div.menu ul { + list-style-type: none; + padding-left: 10px; + padding-right: 10px; +} + +div.menu ul li { + color: #591622; + font-style : italic; + text-decoration : none; + + border-bottom-style: solid; + border-color: #cb8080; + margin-bottom: 15px; +} + +div.menu ul li a { + display: block; + text-align: right; + text-decoration: none; + vertical-align: middle; + height: 45px; + background-repeat: no-repeat; +} + +a.menu:hover { + color: #591622; + text-decoration : none; + background-color: #ecf6f9; +} + +/* news */ + +div.news ul { + padding-left: 0px; + list-style: inside; +} + +div.news span.date { + font-style: italic; +} + +/* fancy classes */ + +samp.tiny { + font-size: 8pt; +} + +ul.wide li { + padding-bottom: 5px; +} + +.center { + text-align: center; +} + +div.topimage { + text-align: left; + padding-top: 28px; + padding-bottom: 28px; +} + +div.bottombar { + display: block; + width: auto; + margin-top: 40px; +} + +div.uplined { + height: auto; + padding-top: 10px; + width: 40%; + border-color: #cb8080; + border-top-style: solid; + border-top-width: 3px; +} + +a.quiet:link,visited,hover { + background-color: transparent; + text-decoration: none; + border-style: none; +} + +a.quiet img { + border-style:none; +} + +span.screenshots { + float: right; +} + +/* papers */ + +li.paper { + padding-bottom: 5px; +} + +span.paper_info { + display: block; +} +span.paper_abstract { + display: none; +} +span.paper_abstract:before { + content: "Abstract: "; + font-weight: bold; + font-style: normal; +} +span.paper_download { + display: block; + float: right; +} +a.paper_download { /* snipet from ikiwiki rss button, thanks! */ + background: #ff6600; + color: white !important; + border-left: 0.5px solid #cc9966; + border-top: 1px solid #ccaa99; + border-right: 1px solid #993300; + border-bottom: 1px solid #331100; + padding: 0px 0.5em 0px 0.5em; + font-family: helvetica, arial, sans-serif; + font-size: 80%; + text-decoration: none; + margin-top: 1em; +} + +span.paper_author { + font-style: italic; +} + +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/matita1.0/theses.shtml b/helm/www/matita1.0/theses.shtml new file mode 100644 index 000000000..37a2b4117 --- /dev/null +++ b/helm/www/matita1.0/theses.shtml @@ -0,0 +1,39 @@ + + +

+ + + Cosimo Arndt Oliboni +
+ + Matita come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva + dei Microcontroller a 8 bit Freescale + + + .pdf + + + Undergraduate thesis, University of Bologna, 2008. + + + We describe an executable formalization of the operational semantics of + every microcontroller of the Freescale 8-bit families (HC05, HC08, HCS08, + RS08). The formalization is done in Matita and heavily relies on dependent + types (for static checking) and executable exhaustive tests (to avoid + under-specification and specification errors). Real world programs have + been compiled to assembly (using CodeWarrior) and executed both with + the emulator formalized in Matita and its extracted OCaml version (for + performance reasons). All aspects of memory management and execution are + captured, up to the point of precisely characterizing the number of clock + cycles required by any single instruction. The manuscript is in Italian + only. + +

diff --git a/helm/www/matita1.0/xhtml-header.shtml b/helm/www/matita1.0/xhtml-header.shtml new file mode 100644 index 000000000..3bfa720fb --- /dev/null +++ b/helm/www/matita1.0/xhtml-header.shtml @@ -0,0 +1,5 @@ + + + + diff --git a/helm/www/matita1.0/xhtml-meta.shtml b/helm/www/matita1.0/xhtml-meta.shtml new file mode 100644 index 000000000..5117dd290 --- /dev/null +++ b/helm/www/matita1.0/xhtml-meta.shtml @@ -0,0 +1,2 @@ + + diff --git a/helm/www/matita1.0/xml/papers.xml b/helm/www/matita1.0/xml/papers.xml new file mode 100644 index 000000000..b85999761 --- /dev/null +++ b/helm/www/matita1.0/xml/papers.xml @@ -0,0 +1,156 @@ + + + + + Andrea Asperti + Claudio Sacerdoti Coen + Enrico Tassi + Stefano Zacchiroli + + + The Matita Proof Assistant + + + Matita is a new document-centric proof assistant that integrates several + Mathematical Knowledge Management tools and techniques. In this paper we + describe the architecture of Matita and the peculiarities of its user + interface. + + + Submitted to Journal of + Automated Reasoning, Special Issue on User Interfaces for Theorem + Proving + + + + + + + Claudio Sacerdoti Coen + Enrico Tassi + Stefano Zacchiroli + + + Tinycals: step by step tacticals + + + Most of the state-of-the-art proof assistants are based on procedural + proof languages, scripts, and rely on LCF tacticals as the primary tool + for tactics composition. In this paper we discuss how these ingredients + do not interact well with user interfaces based on the same interaction + paradigm of Proof General (the de facto standard in this field), + identifying in the coarse-grainedness of tactical evaluation the key + problem. + + We propose tinycals as an alternative to a subset of LCF tacticals, + showing that the user does not experience the same problem if tacticals + are evaluated in a more fine-grained manner. We present the formal + operational semantics of tinycals as well as their implementation in the + Matita proof assistant. + + + Submitted to + UITP 2006 + User Interfaces for Theorem Provers. Seattle, WA -- August 21, 2006. + + + + + + + Luca Padovani + Stefano Zacchiroli + + + From notation to semantics: there and back again + + + Mathematical notation is a structured, open, and ambiguous language. In + order to support mathematical notation in MKM applications one must + necessarily take into account presentational as well as semantic aspects. + The former are required to create a familiar, comfortable, and usable + interface to interact with. The latter are necessary in order to process + the information meaningfully. In this paper we investigate a framework + for dealing with mathematical notation in a meaningful, extensible way, + and we show an effective instantiation of its architecture to the field + of interactive theorem proving. The framework builds upon well-known + concepts and widely-used technologies and it can be easily adopted by + other MKM applications. + + + Accepted for publication in the proceedings of + MKM 2006: The + 5th International Conference on Mathematical Knowledge Management. + Wokingham, UK -- August 11-12, 2006. + + + + + + + Andrea Asperti + Ferruccio Guidi + Claudio Sacerdoti Coen + Enrico Tassi + Stefano Zacchiroli + + + A content based mathematical search engine: Whelp + + + The prototype of a content based search engine for mathematical knowledge + supporting a small set of queries requiring matching and/or typing + operations is described. The prototype, called Whelp, exploits a metadata + approach for indexing the information that looks far more flexible than + traditional indexing techniques for structured expressions like + substitution, discrimination, or context trees. The prototype has been + instantiated to the standard library of the Coq proof assistant extended + with many user contributions. + + + In Proceedings of + TYPES 2004 conference Types for + Proofs and Programs. Paris, France -- December 15-18, 2004. + LNCS 3839/2004, Springer-Verlag Heidelberg, ISBN 3-540-31428-8, pp. 17-32 + + + + + + + Claudio Sacerdoti Coen + Stefano Zacchiroli + + + Efficient Ambiguous Parsing of Mathematical Formulae + + + Mathematical notation has the characteristic of being ambiguous: + operators can be overloaded and information that can be deduced is often + omitted. Mathematicians are used to this ambiguity and can easily + disambiguate a formula making use of the context and of their ability to + find the right interpretation. + + Software applications that have to deal with formulae usually avoid these + issues by fixing an unambiguous input notation. This solution is annoying + for mathematicians because of the resulting tricky syntaxes and becomes a + show stopper to the simultaneous adoption of tools characterized by + different input languages. + + In this paper we present an efficient algorithm suitable for ambiguous + parsing of mathematical formulae. The only requirement of the algorithm + is the existence of a validity predicate over abstract syntax trees of + incomplete formulae with placeholders. This requirement can be easily + fulfilled in the applicative area of interactive proof assistants, and in + several other areas of Mathematical Knowledge Management. + + + In Proceedings of MKM 2004 + Third International Conference on Mathematical Knowledge Management. + September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004, + Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362 + + + + + diff --git a/helm/www/matita1.0/xsl/papers2xhtml.xsl b/helm/www/matita1.0/xsl/papers2xhtml.xsl new file mode 100644 index 000000000..f0f278c3e --- /dev/null +++ b/helm/www/matita1.0/xsl/papers2xhtml.xsl @@ -0,0 +1,70 @@ + + + + + +

+ + + +

+ +
+ + + paper_download + + papers/ + + .pdf + + .pdf + + + paper_download + + papers/ + + .ps + + .ps + +
+ +
+ +

+ + + + + + + + , + + + + + + + + + + + + + + + + + + + + + + + +