]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/dist/INSTALL
0.5.1 should be realased soon, the bug that was affecting fixpoints
[helm.git] / helm / software / matita / dist / INSTALL
index ddc50467e2211f9cb5d9cf1b5e9205dee90fb34e..2a1533815c40f712f946cba973761cb15b343403 100644 (file)
@@ -1,3 +1,11 @@
+Tiny Matita logoMatita Home
+
+                           Chapter 2. Installation
+Prev                                                                      Next
+
+━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
+
 Chapter 2. Installation
 
 Table of Contents
@@ -6,9 +14,11 @@ Installing from sources
 
     Getting the source code
     Requirements
-    Database setup
+    (optional) MySQL setup
     Compiling and installing
 
+Configuring Matita
+
 Installing from sources
 
 Currently, the only intended way to install Matita is starting from its source
@@ -32,16 +42,18 @@ Requirements
 In order to build Matita from sources you will need some tools and libraries.
 They are listed below.
 
-Note for Debian 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:
+Note for Debian (and derivatives) users
 
-              deb http://people.debian.org/~zack unstable helm
+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.
 
+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
 
@@ -82,9 +94,12 @@ MySQL , OCaml MySQL
 
     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
 
@@ -99,11 +114,11 @@ CamlZip
 
     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,
@@ -132,49 +147,50 @@ This will check that all needed tools and library are installed and prepare the
 sources for compilation and installation.
 
 Quite a few (optional) arguments may be passed to the configure command line to
-change build time parameters. They are listed in the table below, together with
-their default values.
-
-Table 2.1.  configure command line arguments
-
-┌──────────────────┬─────────┬────────────────────────────────────────────────┐
-│     Argument     │ Default │                  Description                   │
-├──────────────────┼─────────┼────────────────────────────────────────────────┤
-│--with-runtime-dir│/usr/    │Runtime base directory where all Matita stuff   │
-│=dir              │local/   │(executables, configuration files, standard     │
-│                  │matita/  │library, ...) will be installed                 │
-├──────────────────┼─────────┼────────────────────────────────────────────────┤
-│                  │         │Default SQL server hostname. Will be used while │
-│                  │         │building the standard library during the        │
-│--with-dbhost=host│localhost│installation and to create the default Matita   │
-│                  │         │configuration. May be changed later in          │
-│                  │         │configuration file.                             │
-├──────────────────┼─────────┼────────────────────────────────────────────────┤
-│--enable-debug    │disabled │Enable debugging code. Not for the casual user. │
-└──────────────────┴─────────┴────────────────────────────────────────────────┘
+change build time parameters. They are listed below, together with their
+default values:
+
+configure command line arguments
+
+--with-runtime-dir=dir
+
+    (Default: /usr/local/matita) Runtime base directory where all Matita stuff
+    (executables, configuration files, standard library, ...) will be installed
+
+--with-dbhost=host
+
+    (Default: localhost) Default SQL server hostname. Will be used while
+    building the standard library during the installation and to create the
+    default Matita configuration. May be changed later in configuration file.
+
+--enable-debug
+
+    (Default: disabled) Enable debugging code. Not for the casual user.
 
 Then you will manage the build and install process using make as usual. Below
-are reported the targets you have to invoke in sequence to build and install.
+are reported the targets you have to invoke in sequence to build and install:
 
 make targets
 
 world
 
-    builds components needed by Matita and Matita itself (in bytecode only or
-    in both bytecode and native code depending on the availability of the OCaml
-    native code compiler)
+    builds components needed by Matita and Matita itself (in bytecode or native
+    code depending on the availability of the OCaml native code compiler)
 
-library
+install
 
-    uses the (just built) matitac compiler to build the Matita standard
-    library.
+    installs Matita related tools, standard library and the needed runtime
+    stuff in the proper places on the filesystem.
+
+    As a part of the installation process the Matita standard library will be
+    compiled, thus testing that the just built matitac compiler works properly.
 
     For this step you will need a working SQL database (for indexing the
     standard library while you are compiling it). See Database setup for
     instructions on how to set it up.
 
-install
+━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
 
-    installs Matita related tools, standard library and the needed runtime
-    stuff in the proper places on the filesystem
+Prev                                                                       Next
+Matita vs Coq                        Home                    Configuring Matita