X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_install.xml;h=92e9d62cc178812ca621194e31b49dd40b8e2903;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=35d7ff900a6d3771b9b1b00825533493603710f6;hpb=e15e22b0bb0723470473e37ccbcd75b90494c614;p=helm.git diff --git a/helm/software/matita/help/C/sec_install.xml b/helm/software/matita/help/C/sec_install.xml index 35d7ff900..92e9d62cc 100644 --- a/helm/software/matita/help/C/sec_install.xml +++ b/helm/software/matita/help/C/sec_install.xml @@ -1,16 +1,199 @@ - + Installation - - Installing &appname; from sources - - Currently, the only intended way to install &appname; is starting - from its source code. - - + + &appname; is a quite complex piece of software, we thus recommend + you to either install al precompiled version or use the LiveCD. + If you are running Debian GNU/Linux (or one of its derivatives + like Ubuntu), you can install matita typing + + If you are running MacOSX or Windows, give the LiveCD a try before + trying to compile &appname; from its sources. + + + + Using the LiveCD + + + In the following, we will assume you have installed + virtualbox + for your platform and downloaded the .iso image of the LiveCD + + + + Creating the virtual machine + + Click on the New button, a wizard will popup, you should ask to + its questions as follows + + + The name should be something like &appname;, but can + be any meaningful string. + + + The OS type should be Debian + + + The base memory size can be 256 mega bytes, but you may + want to increase it if you are going to work with huge + formalizations. + + + The boot hard disk should be no hard disk. It may complain + that this choice is not common, but it is right, since you + will run a LiveCD you do not need to emulate an hard drive. + + + Now that you are done with the creation of the virtual machine, + you need to insert the LiveCD in the virtual cd reader unit. + +
The brand new virtual machine + + + + + The breand new virtual machine + +
+ + Click on CD/DVD-ROM (that should display something like: Not mouted). + Then click on mount CD/DVD drive and select the ISO image + option. The combo-box should display no available image, you need to + add the ISO image you downloaded from the &appname; website clicking on + the button near the combo-box. + to start the virtual machine. + +
Mounting an ISO image + + + + + Mounting an ISO image + +
+ + In the newely opened window click + the Add button + +
Choosing the ISO image + + + + + Choosing the ISO image + +
+ + A new windows will pop-up: choose the file you downloaded + (usually matita-version.iso) and click open. + +
Choosing the ISO image + + + + + Choosing the ISO image + +
+ + Now select the new entry you just added as the CD image + you want to insert in the virtual CD drive. + You are now ready to start the virtual machine. + + + + Sharing files with the real PC + + The virtual machine &appname; will run on, has its own file + system, that is completely separated from the one of your + real PC (thus your files are not available in the + emulated environment) and moreover it is a non-presistent + file system (thus you data is lost every time you + turn off the virtual machine). + + + Virtualbox allows you to share a real folder (beloging + to your real PC) with the emulated computer. Since this + folder is persistent, you are encouraged to put + your work there, so that it is not lost when the virtual + machine is powered off. + + + The first step to set up a shared folder is to click + on the shared folder configuration entry + of the virtual machine. + +
Set up a shared folder + + + + + Shared folder + +
+ + Then you shuld add a shared folder clicking on the + plus icon on the right + +
Choosing the folder to share + + + + + Shared folder + +
+ + Then you have to specify the real PC folder you want to share + and name it. A reasonable folder to share is /home on + a standard Unix system, while /Users on MaxOSX. + The name you give to the share is important, you should + remember it. + +
Naming the shared folder + + + + + Shared folder + +
+ + Once your virtual machine is up and running, you can + mount (that meand have access to) the shared folder + by clicking on the Mount VirtualBox share icon, and typing + the name of the share. + +
Using it from the virtual machine + + + + + Shared folder at work + +
+ + A window will then pop-up, and its content will be the + the content of the real PC folder. + + + + + + + Installing from sources + + Install &appname; from the sources is hard, you have been warned! + + + Getting the source code You can get the &appname; source code in two ways: @@ -38,26 +221,33 @@ - + - + Requirements In order to build &appname; 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: - 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. + @@ -171,10 +361,7 @@ - - MySQL - + &MYSQL; OCaml @@ -184,9 +371,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 + @@ -205,7 +405,7 @@ ulex + url="http://www.cduce.org/download.html">ulex @@ -216,7 +416,7 @@ CamlZip + url="http://cristal.inria.fr/~xleroy/software.html">CamlZip @@ -227,36 +427,111 @@ - + + + + (optional) &MYSQL; setup + + 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. + + 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, a new database can be created executing + mysqladmin create matita + (matita is the default database name, you can + change it using the db.user key of the + configuration file). + + Then you need to grant the necessary access permissions to the + database user of &appname;, typing echo "grant all privileges + on matita.* to helm;" | mysql matita should do the trick + (helm is the default user name used by &appname; to + access the database, you can change it using the + db.user key of the configuration file). + + + + This way you create a database named matita + on which anyone claiming to be the helm user can + do everything (like adding dummy data or destroying the contained + one). It is strongly suggested to apply more fine grained permissions, + how to do it is out of the scope of this manual. + + + - - Instructions + + Compiling and installing Once you get the source code the installations steps should be quite familiar. First of all you need to configure the build process executing ./configure. This will check that all needed - tools and library are installed. You may need to pass on the command - line some of the parameters riported below: + 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 below, together with their + default values: - <application>configure</application> parameters + <application>configure</application> command line + arguments - &TODO; - &TODO; + + --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 process using 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: + <application>make</application> targets @@ -265,37 +540,145 @@ world builds components needed by &appname; and &appname; itself - (in bytecode only or in both bytecode and native code depending + (in bytecode or native code depending on the availability of the OCaml native code compiler) - - library - - uses the (just built) matitac - compiler to build the &appname; standard library. - For this step you will need a working SQL database (for - indexing the standard library while you are compiling it). See - &TODO; for instructions on how to set it up. - - - install installs &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 + for instructions on how to set it up. - - - - - - + + + + + + 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. + +
Configuring the Databases + + + + + How to configure the databases. + +
+ 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. + + + +