X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_install.xml;h=7dc37937b7525a8e0df725a5a32eb16b337858bd;hb=34d2f477be65e3fd26bfb6d43a3dd0807274549b;hp=38218c190be3496e219eb0f35e0bb333d106575e;hpb=aef659e5893b4bf8c8544d0c54714e10f5b5493a;p=helm.git
diff --git a/helm/software/matita/help/C/sec_install.xml b/helm/software/matita/help/C/sec_install.xml
index 38218c190..7dc37937b 100644
--- a/helm/software/matita/help/C/sec_install.xml
+++ b/helm/software/matita/help/C/sec_install.xml
@@ -47,17 +47,24 @@
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:
- deb http://people.debian.org/~zack unstable helm
- and installing the
- helm-matita-deps package.
+ Note for Debian (and derivatives) users
+
+ 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
+
+
+ An official debian package is going to be added to the
+ archive too.
+
@@ -181,9 +188,22 @@
SQL database and OCaml bindings for its client-side library
The SQL database itself is not strictly needed to run
- &appname;, 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.
+ &appname;, but the client libraries are.
+
+
+
+
+ &Sqlite;
+
+
+
+ OCaml Sqlite3
+
+
+
+ Sqlite database and OCaml bindings
+
@@ -202,7 +222,7 @@
ulex
+ url="http://www.cduce.org/download.html">ulex
@@ -213,7 +233,7 @@
CamlZip
+ url="http://cristal.inria.fr/~xleroy/software.html">CamlZip
@@ -227,10 +247,11 @@
- Database setup
+ (optional) &MYSQL; setup
- To fully exploit &appname; indexing and search capabilities you
- will need a working &MYSQL; database. Detalied instructions on how to do
+ To fully exploit &appname; 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.
@@ -274,57 +295,60 @@
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.
+ parameters. They are listed below, together with their
+ default values:
-
+ configure command line
arguments
-
-
-
- Argument
- Default
- Description
-
-
-
-
-
- --with-runtime-dir=dir
-
- /usr/local/matita/
- Runtime base directory where all &appname; stuff
- (executables, configuration files, standard
- library, ...) will be installed
-
-
-
- --with-dbhost=host
-
- localhost
- Default SQL server hostname. Will be used while
- building the standard library during the installation and to
- create the default &appname; configuration. May be changed
- later in configuration file.
-
-
- --enable-debug
- disabled
- Enable debugging code. Not for the casual user.
-
-
-
-
-
-
+
+
+ --with-runtime-dir=dir
+
+
+
+ (Default:
+ /usr/local/matita) Runtime base directory
+ where all &appname; 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 &appname;
+ 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.
+ to build and install:
+ make targets
@@ -338,20 +362,16 @@
-
- library
-
- uses the (just built) matitac
- compiler to build the &appname; standard library.
-
-
-
installinstalls &appname; related tools, standard library and the
- needed runtime stuff in the proper places on the filesystem
+ needed runtime stuff in the proper places on the filesystem.
+ As a part of the installation process the &appname;
+ 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
@@ -361,11 +381,121 @@
-
-
+
+
+ Configuring &appname;
+
+ The configuration file is divided in four sections. The user and
+ matita ones are self explicative and does not need user
+ intervention. Here we report a sample snippet for these two
+ sections. The remaining db and getter sections will be explained in
+ details later.
+
+
+ $(HOME)
+ $(USER)
+
+
+ $(user.home)/.matita
+ /usr/share/matita/
+ $(user.name)
+
+]]>
+
+
+ &appname; needs to store/fetch data and metadata. Data is essentially
+ composed of XML files, metadata is a set of tuples for a relational
+ model. Data and metadata can produced by the user or be already
+ available. Both kind of data/metadata can be local and/or remote.
+
+
+ The db section tells &appname; where to store and retrieve metadata,
+ while the getter section describes where XML files have to be
+ found. The following picture describes the suggested configuration.
+ Dashed arrows are determined by the configuration file.
+
+
+ The getter
+
+ Consider the following snippet and the URI
+ cic:/matita/foo/bar.con. If &appname;
+ is asked to read that object it will resolve the object trough
+ the getter. Since the first two entries are equally specific
+ (longest match rule applies) first the path
+ file://$(matita.rt_base_dir)/xml/standard-library/foo/bar.con
+ and then file://$(user.home)/.matita/xml/matita/foo/bar.con
+ are inspected.
+
+
+ $(user.home)/.matita/getter/cache
+
+ cic:/matita/
+ file://$(matita.rt_base_dir)/xml/standard-library/
+ ro
+
+
+ cic:/matita/
+ file://$(user.home)/.matita/xml/matita/
+
+
+ cic:/Coq/
+ http://mowgli.cs.unibo.it/xml/
+ legacy
+
+
+]]>
+
+ if the same URI has to be written, the former prefix is skipped
+ since it is marked as readonly (ro).
+ Objects resolved using the third prefix are readonly too, and are
+ retrieved using the network. There is no limit to the number of
+ prefixes the user can define. The distinction between prefixes marked
+ as readonly and legacy is that, legacy ones are really read only, while
+ the ones marked with ro are considered for
+ writing when &appname; is started in system mode (used to publish user
+ developments in the library space).
+
+ The db
+
+ The database subsystem has three fron ends: library, user and
+ legacy. The latter is the only optional one. Every query is done on
+ every frontend, making the duplicate free union of the results.
+ The user front end kepps metadata produced by the user, and is thus
+ heavily accessed in read/write mode, while the library and legacy
+ fron ends are read only. Every front end can be connected to
+ backend, the storage actually.
+ Consider the following snippet.
+
+
+ mysql://mowgli.cs.unibo.it matita helm none legacy
+ file://$(matita.rt_base_dir) metadata.db helm helm library
+ file://$(matita.basedir) user.db helm helm user
+
+]]>
+
+ Here the usr database is a file (thus locally accessed trough the
+ Sqlite library) placed in the user's home directory. The library one is
+ placed in the &appname; runtime directory. The legacy fron end is
+ connected to a remote &MYSQL; based storage. Every metadata key
+ takes a path to the storage, the name of the database, the user name,
+ a password (or none) and the name of the front
+ end to which it is attached.
+
+
+