]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/dist/INSTALL
fixed propagation under Fix/Lambda/Case of coercions, better names are
[helm.git] / matita / dist / INSTALL
index ddc50467e2211f9cb5d9cf1b5e9205dee90fb34e..dfec3e1410805552404e62730cded8a4a131419e 100644 (file)
@@ -1,3 +1,11 @@
+Tiny Matita logoMatita Home
+
+                           Chapter 2. Installation
+Prev                                                                      Next
+
+━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
+
 Chapter 2. Installation
 
 Table of Contents
 Chapter 2. Installation
 
 Table of Contents
@@ -9,6 +17,8 @@ Installing from sources
     Database setup
     Compiling and installing
 
     Database setup
     Compiling and installing
 
+Configuring Matita
+
 Installing from sources
 
 Currently, the only intended way to install Matita is starting from its source
 Installing from sources
 
 Currently, the only intended way to install Matita is starting from its source
@@ -38,7 +48,7 @@ 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:
 
 the required tools and libraries by adding the following repository to your /
 etc/apt/sources.list:
 
-              deb http://people.debian.org/~zack unstable helm
+              deb http://people.debian.org/~zack unstable helm
 
 
 and installing the helm-matita-deps package.
 
 
 and installing the helm-matita-deps package.
@@ -132,49 +142,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
 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
 
 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
 
 
 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)
+
+install
 
 
-library
+    installs Matita related tools, standard library and the needed runtime
+    stuff in the proper places on the filesystem.
 
 
-    uses the (just built) matitac compiler to build the Matita standard
-    library.
+    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.
 
 
     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