0.5.1 should be realased soon, the bug that was affecting fixpoints

disambiguation is nasty

diff --git a/helm/software/configure.ac b/helm/software/configure.ac
index 78a06a8c0c165561f339cb870dd9f4ec52a2e43e..8181acc0ad6ac92cd23cdef6ea82284b43f6be1c 100644 (file)
--- a/helm/software/configure.ac
+++ b/helm/software/configure.ac
@@ -5,7 +5,7 @@ AC_INIT(matita/matitaTypes.ml)
 DEBUG_DEFAULT="true"
 DEFAULT_DBHOST="mysql://mowgli.cs.unibo.it"
 RT_BASE_DIR_DEFAULT="`pwd`/matita"
 DEBUG_DEFAULT="true"
 DEFAULT_DBHOST="mysql://mowgli.cs.unibo.it"
 RT_BASE_DIR_DEFAULT="`pwd`/matita"

-MATITA_VERSION="0.5.0"
+MATITA_VERSION="0.5.1"

 DISTRIBUTED="no"  # "yes" for distributed tarballs
 # End of distribution settings
 
 DISTRIBUTED="no"  # "yes" for distributed tarballs
 # End of distribution settings
 

diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog
index 8f25732530bcee1fe617d4742ede034afe52cbde..d20d37588883a8993d22c12e5329fdb64840d0cd 100644 (file)
--- a/helm/software/matita/dist/ChangeLog
+++ b/helm/software/matita/dist/ChangeLog
@@ -1,3 +1,8 @@
+0.5.1  - -/5/2008 - minor bug fix release
+       * a wrong context was used to refine fixpoints arguments
+         when trying to optimize out the letin (grep for `AvoidLetIn):
+         (let rec f x = Fix... in f t ---> Fix... t)
+

 0.5.0  - 9/5/2008 - bugfix release
        * first release not considered experimental
 
 0.5.0  - 9/5/2008 - bugfix release
        * first release not considered experimental
 

diff --git a/helm/software/matita/dist/INSTALL b/helm/software/matita/dist/INSTALL
index dfec3e1410805552404e62730cded8a4a131419e..2a1533815c40f712f946cba973761cb15b343403 100644 (file)
--- a/helm/software/matita/dist/INSTALL
+++ b/helm/software/matita/dist/INSTALL
@@ -14,7 +14,7 @@ Installing from sources
 
     Getting the source code
     Requirements
 
     Getting the source code
     Requirements

-    Database setup
+    (optional) MySQL setup

     Compiling and installing
 
 Configuring Matita
     Compiling and installing
 
 Configuring Matita


@@ -42,16 +42,18 @@ Requirements
 In order to build Matita from sources you will need some tools and libraries.
 They are listed below.
 
 In order to build Matita from sources you will need some tools and libraries.
 They are listed below.
 

-Note for Debian users
+Note for Debian (and derivatives) users

 
 

-If you are running a Debian GNU/Linux distribution you can have APT install all
-the required tools and libraries by adding the following repository to your /
-etc/apt/sources.list:
+If you are running a Debian GNU/Linux distribution, or any of its derivative
+like Ubuntu, you can use APT to install all the required tools and libraries
+since they are all part of the Debian archive.

 
 

-              deb http://people.debian.org/~zack unstable helm
+apt-get install ocaml ocaml-findlib libgdome2-ocaml-dev liblablgtk2-ocaml-dev
+liblablgtkmathview-ocaml-dev liblablgtksourceview-ocaml-dev
+libsqlite3-ocaml-dev libocamlnet-ocaml-dev libzip-ocaml-dev libhttp-ocaml-dev
+ocaml-ulex08 libexpat-ocaml-dev libmysql-ocaml-dev camlp5

 
 

-
-and installing the helm-matita-deps package.
+An official debian package is going to be added to the archive too.

 
 Required tools and libraries
 
 
 Required tools and libraries
 


@@ -92,9 +94,12 @@ MySQL , OCaml MySQL
 
     SQL database and OCaml bindings for its client-side library
 
 
     SQL database and OCaml bindings for its client-side library
 

-    The SQL database itself is not strictly needed to run Matita, but we
-    stronly encourage its use since a lot of features are disabled without it.
-    Still, the OCaml bindings of the library are needed at compile time.
+    The SQL database itself is not strictly needed to run Matita, but the
+    client libraries are.
+
+Sqlite , OCaml Sqlite3
+
+    Sqlite database and OCaml bindings

 
 Ocamlnet
 
 
 Ocamlnet
 


@@ -109,11 +114,11 @@ CamlZip
 
     OCaml library to access .gz files
 
 
     OCaml library to access .gz files
 

-Database setup
+(optional) MySQL setup

 
 

-To fully exploit Matita indexing and search capabilities you will need a
-working MySQL database. Detalied instructions on how to do it can be found in
-the MySQL documentation. Here you can find a quick howto.
+To fully exploit Matita indexing and search capabilities on a huge metadata set
+you may need a working MySQL database. Detalied instructions on how to do it
+can be found in the MySQL documentation. Here you can find a quick howto.

 
 In order to create a database you need administrator permissions on your MySQL
 installation, usually the root account has them. Once you have the permissions,
 
 In order to create a database you need administrator permissions on your MySQL
 installation, usually the root account has them. Once you have the permissions,