1 <?xml version="1.0" encoding="UTF-8"?>
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
3 <html xmlns="http://www.w3.org/1999/xhtml">
5 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
7 Manual (rev. 0) - Chapter 2. Installation</title>
10 <div class="chapter" lang="en" xml:lang="en">
11 <div class="titlepage">
14 <h2 class="title"><a id="sec_install"></a>Chapter 2. Installation</h2>
20 <b>Table of Contents</b>
25 <a href="#inst_from_src">Installing from sources</a>
32 <a href="#get_source_code">Getting the source code</a>
37 <a href="#build_requirements">Requirements</a>
42 <a href="#database_setup">Database setup</a>
47 <a href="#build_instructions">Compiling and installing</a>
54 <div class="sect1" lang="en" xml:lang="en">
55 <div class="titlepage">
58 <h2 class="title" style="clear: both"><a id="inst_from_src"></a>Installing from sources</h2>
62 <p>Currently, the only intended way to install Matita is starting
63 from its source code. </p>
64 <div class="sect2" lang="en" xml:lang="en">
65 <div class="titlepage">
68 <h3 class="title"><a id="get_source_code"></a>Getting the source code</h3>
72 <p>You can get the Matita source code in two ways:
74 <div class="orderedlist">
77 <p> go to the <a href="http://matita.cs.unibo.it/download.shtml" target="_top">download
78 page</a> and get the <a href="http://matita.cs.unibo.it/sources/matita-latest.tar.gz" target="_top">latest released source tarball</a>;</p>
81 <p> get the development sources from <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2F&sc=0" target="_top">our
82 SVN repository</a>. You will need the
83 <span class="application">components/</span> and
84 <span class="application">matita/</span> directories from the
85 <code class="filename">trunk/helm/software/</code> directory, plus the
86 <code class="filename">configure</code> and <code class="filename">Makefile*</code>
87 stuff from the same directory. </p>
88 <p>In this case you will need to run
89 <span><strong class="command">autoconf</strong></span> before proceding with the building
90 instructions below.</p>
97 <div class="sect2" lang="en" xml:lang="en">
98 <div class="titlepage">
101 <h3 class="title"><a id="build_requirements"></a>Requirements</h3>
105 <p>In order to build Matita from sources you will need some
106 tools and libraries. They are listed below.
109 <div class="note" style="margin-left: 0.5in; margin-right: 0.5in;">
110 <h3 class="title">Note for Debian users</h3>
111 <p>If you are running a <a href="http://www.debian.org" target="_top">Debian GNU/Linux</a> distribution
112 you can have APT install all the required tools and libraries by
113 adding the following repository to your
114 <code class="filename">/etc/apt/sources.list</code>: </p>
115 <pre class="programlisting">
116 deb <a href="http://people.debian.org/~zack" target="_top">http://people.debian.org/~zack</a> unstable helm
118 <p> and installing the
119 <span class="application">helm-matita-deps</span> package.</p>
124 <div class="variablelist">
126 <b>Required tools and libraries</b>
131 <span class="application">
132 <a href="http://caml.inria.fr" target="_top">OCaml</a>
137 <p> the Objective Caml compiler, version 3.09 or above </p>
141 <span class="application">
142 <a href="http://www.ocaml-programming.de/packages/" target="_top">Findlib</a>
147 <p> OCaml package manager, version 1.1.1 or above</p>
151 <span class="application">
152 <a href="http://www.xs4all.nl/~mmzeeman/ocaml/" target="_top">OCaml
158 <p>OCaml bindings for the <span class="application"><a href="http://expat.sourceforge.net/" target="_top">expat</a>
163 <span class="application">
164 <a href="http://gmetadom.sourceforge.net/" target="_top">GMetaDOM</a>
169 <p>OCaml bindings for the <span class="application"><a href="http://gdome2.cs.unibo.it/" target="_top">Gdome 2</a>
174 <span class="application">
175 <a href="http://www.bononia.it/~zack/ocaml-http.en.html" target="_top">OCaml
181 <p> OCaml library to write HTTP daemons (and clients) </p>
185 <span class="application">
186 <a href="http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html" target="_top">LablGTK</a>
191 <p> OCaml bindings for the <span class="application"><a href="http://www.gtk.org" target="_top"> GTK+</a> library
192 </span>, version 2.6.0 or above </p>
195 <span class="term"><span class="application"><a href="http://helm.cs.unibo.it/mml-widget/" target="_top">GtkMathView</a></span>
198 <span class="application">
199 <a href="http://helm.cs.unibo.it/mml-widget/" target="_top">LablGtkMathView</a>
204 <p> GTK+ widget to render <a href="http://www.w3.org/Math/" target="_top">MathML</a> documents and its
208 <span class="term"><span class="application"><a href="http://gtksourceview.sourceforge.net/" target="_top">GtkSourceView</a></span>
211 <span class="application">
212 <a href="http://helm.cs.unibo.it/software/lablgtksourceview/" target="_top">LablGtkSourceView</a>
217 <p> extension for the GTK+ text widget (adding the typical
218 features of source code editors) and its OCaml bindings </p>
221 <span class="term"><span class="application"><a href="http://www.mysql.com" target="_top">MySQL</a></span> , </span>
223 <span class="application">
224 <a href="http://raevnos.pennmush.org/code/ocaml-mysql/" target="_top">OCaml
230 <p> SQL database and OCaml bindings for its client-side library
232 <p> The SQL database itself is not strictly needed to run
233 Matita, but we stronly encourage its use since a lot of
234 features are disabled without it. Still, the OCaml bindings of
235 the library are needed at compile time.</p>
239 <span class="application">
240 <a href="http://ocamlnet.sourceforge.net/" target="_top">Ocamlnet</a>
245 <p> collection of OCaml libraries to deal with
246 application-level Internet protocols and conventions </p>
250 <span class="application">
251 <a href="http://www.cduce.org/download.html#side" target="_top">ulex</a>
256 <p> Unicode lexer generator for OCaml </p>
260 <span class="application">
261 <a href="http://cristal.inria.fr/~xleroy/software.html#camlzip" target="_top">CamlZip</a>
266 <p> OCaml library to access <code class="filename">.gz</code> files
273 <div class="sect2" lang="en" xml:lang="en">
274 <div class="titlepage">
277 <h3 class="title"><a id="database_setup"></a>Database setup</h3>
281 <p> To fully exploit Matita indexing and search capabilities you
282 will need a working <span class="application"><a href="http://www.mysql.com" target="_top">MySQL</a></span> database. Detalied instructions on how to do
283 it can be found in the <a href="http://dev.mysql.com/doc/" target="_top">MySQL documentation</a>. Here you
284 can find a quick howto. </p>
285 <p> In order to create a database you need administrator permissions on
286 your MySQL installation, usually the root account has them. Once you
287 have the permissions, a new database can be created executing
288 <strong class="userinput"><code>mysqladmin create matita</code></strong>
289 (<span class="emphasis"><em>matita</em></span> is the default database name, you can
290 change it using the <em class="parameter"><code>db.user</code></em> key of the
291 configuration file). </p>
292 <p> Then you need to grant the necessary access permissions to the
293 database user of Matita, typing <strong class="userinput"><code>echo "grant all privileges
294 on matita.* to helm;" | mysql matita</code></strong> should do the trick
295 (<span class="emphasis"><em>helm</em></span> is the default user name used by Matita to
296 access the database, you can change it using the
297 <em class="parameter"><code>db.user</code></em> key of the configuration file).
299 <div class="note" style="margin-left: 0.5in; margin-right: 0.5in;">
300 <h3 class="title">Note</h3>
301 <p> This way you create a database named <span class="emphasis"><em>matita</em></span>
302 on which anyone claiming to be the <span class="emphasis"><em>helm</em></span> user can
303 do everything (like adding dummy data or destroying the contained
304 one). It is strongly suggested to apply more fine grained permissions,
305 how to do it is out of the scope of this manual.</p>
308 <div class="sect2" lang="en" xml:lang="en">
309 <div class="titlepage">
312 <h3 class="title"><a id="build_instructions"></a>Compiling and installing</h3>
316 <p> Once you get the source code the installations steps should be
318 <p> First of all you need to configure the build process executing
319 <strong class="userinput"><code>./configure</code></strong>. This will check that all needed
320 tools and library are installed and prepare the sources for compilation
321 and installation. </p>
322 <p> Quite a few (optional) arguments may be passed to the
323 <span class="application">configure</span> command line to change build time
324 parameters. They are listed in the table below, together with their
329 <a id="id2497494"></a>
331 <b>Table 2.1. <span class="application">configure</span> command line
334 <table border="1" summary=" configure command line arguments">
342 <th align="center">Argument</th>
343 <th align="center">Default</th>
344 <th align="center">Description</th>
350 <strong class="userinput">
351 <code>--with-runtime-dir=<em class="replaceable"><code>dir</code></em></code>
355 <code class="filename">/usr/local/matita/</code>
358 <p> Runtime base directory where all Matita stuff
359 (executables, configuration files, standard
360 library, ...) will be installed </p>
365 <strong class="userinput">
366 <code>--with-dbhost=<em class="replaceable"><code>host</code></em></code>
369 <td align="left"> localhost </td>
371 <p>Default SQL server hostname. Will be used while
372 building the standard library during the installation and to
373 create the default Matita configuration. May be changed
374 later in configuration file.</p>
379 <strong class="userinput">
380 <code>--enable-debug</code>
383 <td align="left"> disabled </td>
385 <p> Enable debugging code. Not for the casual user.
395 <p> Then you will manage the build and install process using
396 <span class="application"><a href="http://www.gnu.org/software/make/" target="_top">make</a></span>
397 as usual. Below are reported the targets you have to invoke in sequence
398 to build and install.
401 <div class="variablelist">
403 <b><span class="application">make</span> targets</b>
408 <strong class="userinput">
414 <p>builds components needed by Matita and Matita itself
415 (in bytecode only or in both bytecode and native code depending
416 on the availability of the OCaml native code compiler) </p>
420 <strong class="userinput">
426 <p>uses the (just built) <span class="application">matitac</span>
427 compiler to build the Matita standard library. </p>
428 <p>For this step you will need a working SQL database (for
429 indexing the standard library while you are compiling it). See
430 <a href="#database_setup" target="_top">Database setup</a>
431 for instructions on how to set it up.</p>
435 <strong class="userinput">
441 <p>installs Matita related tools, standard library and the
442 needed runtime stuff in the proper places on the filesystem