From bbd38c52dd50cdaedae5e3e9a53256d3696751aa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 7 Jan 2010 22:53:47 +0000 Subject: [PATCH] ... --- helm/www/matita/Makefile | 17 +++++++++++++++++ helm/www/matita/documentation.shtml | 17 +++++++++++++++-- helm/www/matita/news.shtml | 3 +++ 3 files changed, 35 insertions(+), 2 deletions(-) diff --git a/helm/www/matita/Makefile b/helm/www/matita/Makefile index 4e33738d8..c54475713 100644 --- a/helm/www/matita/Makefile +++ b/helm/www/matita/Makefile @@ -2,6 +2,10 @@ # 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 @@ -15,6 +19,7 @@ all: @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" @@ -30,6 +35,18 @@ manual-stamp: $(DOCS_SRC_DIR)/*.xml $(DOCS_SRC_DIR)/xsl/* $(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 \ diff --git a/helm/www/matita/documentation.shtml b/helm/www/matita/documentation.shtml index c4fbeace6..66aab892c 100644 --- a/helm/www/matita/documentation.shtml +++ b/helm/www/matita/documentation.shtml @@ -48,9 +48,22 @@ available from our repository, in the matita/help/C/ folder.

-

Tutorial

+

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

-

A not so short tutorial by A.Asperti

Exercises

diff --git a/helm/www/matita/news.shtml b/helm/www/matita/news.shtml index bf8f627c8..18743ca3b 100644 --- a/helm/www/matita/news.shtml +++ b/helm/www/matita/news.shtml @@ -3,6 +3,9 @@
News