2 <!-- ============= Installation ============================== -->
4 <chapter id="sec_install">
5 <title>Installation</title>
8 &appname; is a quite complex piece of software, we thus recommend
9 you to either install al precompiled version or use the LiveCD.
10 If you are running Debian GNU/Linux (or one of its derivatives
11 like Ubuntu), you can install matita typing
12 <programlisting><![CDATA[ aptitude install matita matita-standard-library ]]></programlisting>
13 If you are running MacOSX or Windows, give the LiveCD a try before
14 trying to compile &appname; from its sources.
17 <sect1 id="inst_livecd">
18 <title>Using the LiveCD</title>
21 In the following, we will assume you have installed
22 <ulink type="http" url="http://www.virtualbox.org">virtualbox</ulink>
23 for your platform and downloaded the .iso image of the LiveCD
26 <sect2 id="make_vmachine">
27 <title>Creating the virtual machine</title>
29 Click on the New button, a wizard will popup, you should ask to
30 its questions as follows
33 The name should be something like &appname;, but can
34 be any meaningful string.
37 The OS type should be Debian
40 The base memory size can be 256 mega bytes, but you may
41 want to increase it if you are going to work with huge
45 The boot hard disk should be no hard disk. It may complain
46 that this choice is not common, but it is right, since you
47 will run a LiveCD you do not need to emulate an hard drive.
50 Now that you are done with the creation of the virtual machine,
51 you need to insert the LiveCD in the virtual cd reader unit.
53 <figure><title>The brand new virtual machine</title>
56 <imagedata fileref="figures/vbox1.png" format="PNG" srccredit="Enrico Tassi"/>
58 <textobject><phrase>The breand new virtual machine</phrase></textobject>
62 Click on CD/DVD-ROM (that should display something like: Not mouted).
63 Then click on mount CD/DVD drive and select the ISO image
64 option. The combo-box should display no available image, you need to
65 add the ISO image you downloaded from the &appname; website clicking on
66 the button near the combo-box.
67 to start the virtual machine.
69 <figure><title>Mounting an ISO image</title>
72 <imagedata fileref="figures/vbox2.png" format="PNG" srccredit="Enrico Tassi"/>
74 <textobject><phrase>Mounting an ISO image</phrase></textobject>
78 In the newely opened window click
81 <figure><title>Choosing the ISO image</title>
84 <imagedata fileref="figures/vbox3.png" format="PNG" srccredit="Enrico Tassi"/>
86 <textobject><phrase>Choosing the ISO image</phrase></textobject>
90 A new windows will pop-up: choose the file you downloaded
91 (usually matita-version.iso) and click open.
93 <figure><title>Choosing the ISO image</title>
96 <imagedata fileref="figures/vbox35.png" format="PNG" srccredit="Enrico Tassi"/>
98 <textobject><phrase>Choosing the ISO image</phrase></textobject>
102 Now select the new entry you just added as the CD image
103 you want to insert in the virtual CD drive.
104 You are now ready to start the virtual machine.
108 <title>Sharing files with the real PC</title>
110 The virtual machine &appname; will run on, has its own file
111 system, that is completely separated from the one of your
112 real PC (thus your files are not available in the
113 emulated environment) and moreover it is a non-presistent
114 file system (thus you data is lost every time you
115 turn off the virtual machine).
118 Virtualbox allows you to share a real folder (beloging
119 to your real PC) with the emulated computer. Since this
120 folder is persistent, you are encouraged to put
121 your work there, so that it is not lost when the virtual
122 machine is powered off.
125 The first step to set up a shared folder is to click
126 on the shared folder configuration entry
127 of the virtual machine.
129 <figure><title>Set up a shared folder</title>
132 <imagedata fileref="figures/vbox4.png"
133 format="PNG" srccredit="Enrico Tassi"/>
135 <textobject><phrase>Shared folder</phrase></textobject>
139 Then you shuld add a shared folder clicking on the
140 plus icon on the right
142 <figure><title>Choosing the folder to share</title>
145 <imagedata fileref="figures/vbox5.png"
146 format="PNG" srccredit="Enrico Tassi"/>
148 <textobject><phrase>Shared folder</phrase></textobject>
152 Then you have to specify the real PC folder you want to share
153 and name it. A reasonable folder to share is /home on
154 a standard Unix system, while /Users on MaxOSX.
155 The name you give to the share is important, you should
158 <figure><title>Naming the shared folder</title>
161 <imagedata fileref="figures/vbox6.png"
162 format="PNG" srccredit="Enrico Tassi"/>
164 <textobject><phrase>Shared folder</phrase></textobject>
168 Once your virtual machine is up and running, you can
169 mount (that meand have access to) the shared folder
170 by clicking on the Mount VirtualBox share icon, and typing
171 the name of the share.
173 <figure><title>Using it from the virtual machine</title>
176 <imagedata fileref="figures/vbox7.png"
177 format="PNG" srccredit="Enrico Tassi"/>
179 <textobject><phrase>Shared folder at work</phrase></textobject>
183 A window will then pop-up, and its content will be the
184 the content of the real PC folder.
190 <sect1 id="inst_from_src">
191 <title>Installing from sources</title>
193 <para>Install &appname; from the sources is hard, you have been warned!
196 <sect2 id="get_source_code">
197 <title>Getting the source code</title>
199 <para>You can get the &appname; source code in two ways:
202 <listitem> <para> go to the <ulink type="http"
203 url="http://matita.cs.unibo.it/download.shtml">download
204 page</ulink> and get the <ulink type="http"
205 url="http://matita.cs.unibo.it/sources/matita-latest.tar.gz"
206 >latest released source tarball</ulink>;</para> </listitem>
208 <listitem> <para> get the development sources from <ulink type="http"
209 url="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2F&sc=0">our
210 SVN repository</ulink>. You will need the
211 <application>components/</application> and
212 <application>matita/</application> directories from the
213 <filename>trunk/helm/software/</filename> directory, plus the
214 <filename>configure</filename> and <filename>Makefile*</filename>
215 stuff from the same directory. </para>
217 <para>In this case you will need to run
218 <command>autoconf</command> before proceding with the building
219 instructions below.</para> </listitem>
226 <sect2 id="build_requirements">
227 <title>Requirements</title>
229 <para>In order to build &appname; from sources you will need some
230 tools and libraries. They are listed below.
233 <title>Note for Debian (and derivatives) users</title>
235 <para>If you are running a
237 url="http://www.debian.org">Debian GNU/Linux</ulink>
239 or any of its derivative like <ulink type="http"
240 url="http://ubuntu.com">Ubuntu</ulink>,
241 you can use APT to install all the required tools and
242 libraries since they are all part of the Debian archive.
245 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
248 An official debian package is going to be added to the
255 <title>Required tools and libraries</title>
259 <application> <ulink type="http"
260 url="http://caml.inria.fr">OCaml</ulink> </application>
263 <para> the Objective Caml compiler, version 3.09 or above </para>
269 <application> <ulink type="http"
270 url="http://www.ocaml-programming.de/packages/">Findlib</ulink>
274 <para> OCaml package manager, version 1.1.1 or above</para>
280 <application> <ulink type="http"
281 url="http://www.xs4all.nl/~mmzeeman/ocaml/">OCaml
282 Expat</ulink> </application>
285 <para>OCaml bindings for the <application><ulink type="http"
286 url="http://expat.sourceforge.net/">expat</ulink>
287 library</application> </para>
294 <application> <ulink type="http"
295 url="http://gmetadom.sourceforge.net/">GMetaDOM</ulink>
299 <para>OCaml bindings for the <application><ulink type="http"
300 url="http://gdome2.cs.unibo.it/">Gdome 2</ulink>
301 library</application></para>
309 <application> <ulink type="http"
310 url="http://www.bononia.it/~zack/ocaml-http.en.html">OCaml
311 HTTP</ulink> </application>
314 <para> OCaml library to write HTTP daemons (and clients) </para>
321 <application> <ulink type="http"
322 url="http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html">LablGTK</ulink>
326 <para> OCaml bindings for the <application> <ulink type="http"
327 url="http://www.gtk.org"> GTK+</ulink> library
328 </application>, version 2.6.0 or above </para>
335 <application> <ulink type="http"
336 url="http://helm.cs.unibo.it/mml-widget/">GtkMathView</ulink>
340 <application> <ulink type="http"
341 url="http://helm.cs.unibo.it/mml-widget/">LablGtkMathView</ulink>
345 <para> GTK+ widget to render <ulink type="http"
346 url="http://www.w3.org/Math/">MathML</ulink> documents and its
347 OCaml bindings </para>
354 <application> <ulink type="http"
355 url="http://gtksourceview.sourceforge.net/">GtkSourceView</ulink>
359 <application> <ulink type="http"
360 url="http://helm.cs.unibo.it/software/lablgtksourceview/">LablGtkSourceView</ulink>
364 <para> extension for the GTK+ text widget (adding the typical
365 features of source code editors) and its OCaml bindings </para>
371 <term> &MYSQL; </term>
373 <application> <ulink type="http"
374 url="http://raevnos.pennmush.org/code/ocaml-mysql/">OCaml
375 MySQL</ulink> </application>
378 <para> SQL database and OCaml bindings for its client-side library
380 <para> The SQL database itself is not strictly needed to run
381 &appname;, but the client libraries are.</para>
386 <term> &Sqlite; </term>
390 url="http://ocaml.info/home/ocaml_sources.html">
392 </ulink> </application>
395 <para> Sqlite database and OCaml bindings
403 <application> <ulink type="http"
404 url="http://ocamlnet.sourceforge.net/">Ocamlnet</ulink>
408 <para> collection of OCaml libraries to deal with
409 application-level Internet protocols and conventions </para>
415 <application> <ulink type="http"
416 url="http://www.cduce.org/download.html">ulex</ulink>
420 <para> Unicode lexer generator for OCaml </para>
426 <application> <ulink type="http"
427 url="http://cristal.inria.fr/~xleroy/software.html">CamlZip</ulink>
431 <para> OCaml library to access <filename>.gz</filename> files
436 </variablelist> </para>
441 <sect2 id="database_setup">
442 <title>(optional) &MYSQL; setup</title>
444 <para> To fully exploit &appname; indexing and search capabilities
445 on a huge metadata set you may
446 need a working &MYSQL; database. Detalied instructions on how to do
447 it can be found in the <ulink type="http"
448 url="http://dev.mysql.com/doc/">MySQL documentation</ulink>. Here you
449 can find a quick howto. </para>
451 <para> In order to create a database you need administrator permissions on
452 your MySQL installation, usually the root account has them. Once you
453 have the permissions, a new database can be created executing
454 <userinput>mysqladmin create matita</userinput>
455 (<emphasis>matita</emphasis> is the default database name, you can
456 change it using the <parameter>db.user</parameter> key of the
457 configuration file). </para>
459 <para> Then you need to grant the necessary access permissions to the
460 database user of &appname;, typing <userinput>echo "grant all privileges
461 on matita.* to helm;" | mysql matita</userinput> should do the trick
462 (<emphasis>helm</emphasis> is the default user name used by &appname; to
463 access the database, you can change it using the
464 <parameter>db.user</parameter> key of the configuration file).
468 <para> This way you create a database named <emphasis>matita</emphasis>
469 on which anyone claiming to be the <emphasis>helm</emphasis> user can
470 do everything (like adding dummy data or destroying the contained
471 one). It is strongly suggested to apply more fine grained permissions,
472 how to do it is out of the scope of this manual.</para>
478 <sect2 id="build_instructions">
479 <title>Compiling and installing</title>
481 <para> Once you get the source code the installations steps should be
482 quite familiar.</para>
484 <para> First of all you need to configure the build process executing
485 <userinput>./configure</userinput>. This will check that all needed
486 tools and library are installed and prepare the sources for compilation
487 and installation. </para>
489 <para> Quite a few (optional) arguments may be passed to the
490 <application>configure</application> command line to change build time
491 parameters. They are listed below, together with their
492 default values: </para>
495 <title> <application>configure</application> command line
500 <userinput>--with-runtime-dir=<replaceable>dir</replaceable></userinput>
504 (<emphasis>Default:</emphasis>
505 <filename>/usr/local/matita</filename>) Runtime base directory
506 where all &appname; stuff (executables, configuration files,
507 standard library, ...) will be installed
515 <userinput>- - with-dbhost=<replaceable>host</replaceable></userinput>
519 (<emphasis>Default:</emphasis> localhost) Default SQL server
520 hostname. Will be used while building the standard library
521 during the installation and to create the default &appname;
522 configuration. May be changed later in configuration file.
530 <userinput>--enable-debug</userinput>
534 (<emphasis>Default:</emphasis> disabled) Enable debugging code.
535 Not for the casual user.
541 <para> Then you will manage the build and install process using
542 <application><ulink type="http"
543 url="http://www.gnu.org/software/make/">make</ulink></application>
544 as usual. Below are reported the targets you have to invoke in sequence
545 to build and install:
549 <title><application>make</application> targets</title>
552 <term><userinput>world</userinput></term>
554 <para>builds components needed by &appname; and &appname; itself
555 (in bytecode or native code depending
556 on the availability of the OCaml native code compiler) </para>
561 <term><userinput>install</userinput></term>
563 <para>installs &appname; related tools, standard library and the
564 needed runtime stuff in the proper places on the filesystem.
567 <para>As a part of the installation process the &appname;
568 standard library will be compiled, thus testing that the just
569 built <application>matitac</application> compiler works
571 <para>For this step you will need a working SQL database (for
572 indexing the standard library while you are compiling it). See
573 <ulink type="http" url="#database_setup">Database setup</ulink>
574 for instructions on how to set it up.
586 <sect1 id="matita.conf.xml">
587 <title>Configuring &appname;</title>
589 The configuration file is divided in four sections. The user and
590 matita ones are self explicative and does not need user
591 intervention. Here we report a sample snippet for these two
592 sections. The remaining db and getter sections will be explained in
596 <section name="user">
597 <key name="home">$(HOME)</key>
598 <key name="name">$(USER)</key>
600 <section name="matita">
601 <key name="basedir">$(user.home)/.matita</key>
602 <key name="rt_base_dir">/usr/share/matita/</key>
603 <key name="owner">$(user.name)</key>
608 &appname; needs to store/fetch data and metadata. Data is essentially
609 composed of XML files, metadata is a set of tuples for a relational
610 model. Data and metadata can produced by the user or be already
611 available. Both kind of data/metadata can be local and/or remote.
614 The db section tells &appname; where to store and retrieve metadata,
615 while the getter section describes where XML files have to be
616 found. The following picture describes the suggested configuration.
617 Dashed arrows are determined by the configuration file.
619 <figure><title>Configuring the Databases</title>
622 <imagedata fileref="figures/database.png" format="PNG" srccredit="Enrico Tassi"/>
624 <textobject><phrase>How to configure the databases.</phrase></textobject>
627 <para>The getter</para>
629 Consider the following snippet and the URI
630 <userinput>cic:/matita/foo/bar.con</userinput>. If &appname;
631 is asked to read that object it will resolve the object trough
632 the getter. Since the first two entries are equally specific
633 (longest match rule applies) first the path
634 <userinput>file://$(matita.rt_base_dir)/xml/standard-library/foo/bar.con</userinput>
635 and then <userinput>file://$(user.home)/.matita/xml/matita/foo/bar.con</userinput>
639 <section name="getter">
640 <key name="cache_dir">$(user.home)/.matita/getter/cache</key>
643 file://$(matita.rt_base_dir)/xml/standard-library/
648 file://$(user.home)/.matita/xml/matita/
652 http://mowgli.cs.unibo.it/xml/
658 if the same URI has to be written, the former prefix is skipped
659 since it is marked as readonly (<userinput>ro</userinput>).
660 Objects resolved using the third prefix are readonly too, and are
661 retrieved using the network. There is no limit to the number of
662 prefixes the user can define. The distinction between prefixes marked
663 as readonly and legacy is that, legacy ones are really read only, while
664 the ones marked with <userinput>ro</userinput> are considered for
665 writing when &appname; is started in system mode (used to publish user
666 developments in the library space).
670 The database subsystem has three fron ends: library, user and
671 legacy. The latter is the only optional one. Every query is done on
672 every frontend, making the duplicate free union of the results.
673 The user front end kepps metadata produced by the user, and is thus
674 heavily accessed in read/write mode, while the library and legacy
675 fron ends are read only. Every front end can be connected to
676 backend, the storage actually.
677 Consider the following snippet.
681 <key name="metadata">mysql://mowgli.cs.unibo.it matita helm none legacy</key>
682 <key name="metadata">file://$(matita.rt_base_dir) metadata.db helm helm library</key>
683 <key name="metadata">file://$(matita.basedir) user.db helm helm user</key>
687 Here the usr database is a file (thus locally accessed trough the
688 Sqlite library) placed in the user's home directory. The library one is
689 placed in the &appname; runtime directory. The legacy fron end is
690 connected to a remote &MYSQL; based storage. Every metadata key
691 takes a path to the storage, the name of the database, the user name,
692 a password (or <userinput>none</userinput>) and the name of the front
693 end to which it is attached.