1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Installing from sources</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets V1.78.1" /><link rel="home" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="up" href="sec_install.html" title="Chapter 2. Installation" /><link rel="prev" href="sec_install.html" title="Chapter 2. Installation" /><link rel="next" href="matita.conf.xml.html" title="Configuring Matita" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Installing from sources</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_install.html">Prev</a> </td><th width="60%" align="center">Chapter 2. Installation</th><td width="20%" align="right"> <a accesskey="n" href="matita.conf.xml.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="inst_from_src"></a>Installing from sources</h2></div></div></div><p>Install Matita from the sources is hard, you have been warned!
3 </p><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="get_source_code"></a>Getting the source code</h3></div></div></div><p>You can get the Matita source code in two ways:
4 </p><div class="orderedlist"><ol class="orderedlist" type="1"><li class="listitem"><p> go to the <a class="ulink" href="http://matita.cs.unibo.it/download.shtml" target="_top">download
5 page</a> and get the <a class="ulink" href="http://matita.cs.unibo.it/sources/matita-latest.tar.gz" target="_top">latest released source tarball</a>;</p></li><li class="listitem"><p> get the development sources from <a class="ulink" href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2F&sc=0" target="_top">our
6 SVN repository</a>. You will need the
7 <span class="application">components/</span> and
8 <span class="application">matita/</span> directories from the
9 <code class="filename">trunk/helm/software/</code> directory, plus the
10 <code class="filename">configure</code> and <code class="filename">Makefile*</code>
11 stuff from the same directory. </p><p>In this case you will need to run
12 <span class="command"><strong>autoconf</strong></span> before proceding with the building
13 instructions below.</p></li></ol></div><p>
14 </p></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="build_requirements"></a>Requirements</h3></div></div></div><p>In order to build Matita from sources you will need some
15 tools and libraries. They are listed below.
17 </p><div class="note" style="margin-left: 0.5in; margin-right: 0.5in;"><h3 class="title">Note for Debian (and derivatives) users</h3><p>If you are running a
18 <a class="ulink" href="http://www.debian.org" target="_top">Debian GNU/Linux</a>
20 or any of its derivative like <a class="ulink" href="http://ubuntu.com" target="_top">Ubuntu</a>,
21 you can use APT to install all the required tools and
22 libraries since they are all part of the Debian archive.
24 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
26 An official debian package is going to be added to the
30 </p><div class="variablelist"><p class="title"><strong>Required tools and libraries</strong></p><dl class="variablelist"><dt><span class="term">
31 <span class="application"> <a class="ulink" href="http://caml.inria.fr" target="_top">OCaml</a> </span>
32 </span></dt><dd><p> the Objective Caml compiler, version 3.09 or above </p></dd><dt><span class="term">
33 <span class="application"> <a class="ulink" href="http://www.ocaml-programming.de/packages/" target="_top">Findlib</a>
35 </span></dt><dd><p> OCaml package manager, version 1.1.1 or above</p></dd><dt><span class="term">
36 <span class="application"> <a class="ulink" href="http://www.xs4all.nl/~mmzeeman/ocaml/" target="_top">OCaml
38 </span></dt><dd><p>OCaml bindings for the <span class="application"><a class="ulink" href="http://expat.sourceforge.net/" target="_top">expat</a>
39 library</span> </p></dd><dt><span class="term">
40 <span class="application"> <a class="ulink" href="http://gmetadom.sourceforge.net/" target="_top">GMetaDOM</a>
42 </span></dt><dd><p>OCaml bindings for the <span class="application"><a class="ulink" href="http://gdome2.cs.unibo.it/" target="_top">Gdome 2</a>
43 library</span></p></dd><dt><span class="term">
44 <span class="application"> <a class="ulink" href="http://www.bononia.it/~zack/ocaml-http.en.html" target="_top">OCaml
46 </span></dt><dd><p> OCaml library to write HTTP daemons (and clients) </p></dd><dt><span class="term">
47 <span class="application"> <a class="ulink" href="http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html" target="_top">LablGTK</a>
49 </span></dt><dd><p> OCaml bindings for the <span class="application"> <a class="ulink" href="http://www.gtk.org" target="_top"> GTK+</a> library
50 </span>, version 2.6.0 or above </p></dd><dt><span class="term">
51 <span class="application"> <a class="ulink" href="http://helm.cs.unibo.it/mml-widget/" target="_top">GtkMathView</a>
53 , </span><span class="term">
54 <span class="application"> <a class="ulink" href="http://helm.cs.unibo.it/mml-widget/" target="_top">LablGtkMathView</a>
56 </span></dt><dd><p> GTK+ widget to render <a class="ulink" href="http://www.w3.org/Math/" target="_top">MathML</a> documents and its
57 OCaml bindings </p></dd><dt><span class="term">
58 <span class="application"> <a class="ulink" href="http://gtksourceview.sourceforge.net/" target="_top">GtkSourceView</a>
60 , </span><span class="term">
61 <span class="application"> <a class="ulink" href="http://helm.cs.unibo.it/software/lablgtksourceview/" target="_top">LablGtkSourceView</a>
63 </span></dt><dd><p> extension for the GTK+ text widget (adding the typical
64 features of source code editors) and its OCaml bindings </p></dd><dt><span class="term"> <span class="application"> <a class="ulink" href="http://www.mysql.com" target="_top">MySQL</a> </span> , </span><span class="term">
65 <span class="application"> <a class="ulink" href="http://raevnos.pennmush.org/code/ocaml-mysql/" target="_top">OCaml
67 </span></dt><dd><p> SQL database and OCaml bindings for its client-side library
68 </p><p> The SQL database itself is not strictly needed to run
69 Matita, but the client libraries are.</p></dd><dt><span class="term"> <span class="application"> <a class="ulink" href="http://www.sqlite.org" target="_top">Sqlite</a> </span> , </span><span class="term">
70 <span class="application">
71 <a class="ulink" href="http://ocaml.info/home/ocaml_sources.html" target="_top">
74 </span></dt><dd><p> Sqlite database and OCaml bindings
75 </p></dd><dt><span class="term">
76 <span class="application"> <a class="ulink" href="http://ocamlnet.sourceforge.net/" target="_top">Ocamlnet</a>
78 </span></dt><dd><p> collection of OCaml libraries to deal with
79 application-level Internet protocols and conventions </p></dd><dt><span class="term">
80 <span class="application"> <a class="ulink" href="http://www.cduce.org/download.html" target="_top">ulex</a>
82 </span></dt><dd><p> Unicode lexer generator for OCaml </p></dd><dt><span class="term">
83 <span class="application"> <a class="ulink" href="http://cristal.inria.fr/~xleroy/software.html" target="_top">CamlZip</a>
85 </span></dt><dd><p> OCaml library to access <code class="filename">.gz</code> files
86 </p></dd></dl></div><p> </p></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="database_setup"></a>(optional) <span class="application"> <a class="ulink" href="http://www.mysql.com" target="_top">MySQL</a> </span> setup</h3></div></div></div><p> To fully exploit Matita indexing and search capabilities
87 on a huge metadata set you may
88 need a working <span class="application"> <a class="ulink" href="http://www.mysql.com" target="_top">MySQL</a> </span> database. Detalied instructions on how to do
89 it can be found in the <a class="ulink" href="http://dev.mysql.com/doc/" target="_top">MySQL documentation</a>. Here you
90 can find a quick howto. </p><p> In order to create a database you need administrator permissions on
91 your MySQL installation, usually the root account has them. Once you
92 have the permissions, a new database can be created executing
93 <strong class="userinput"><code>mysqladmin create matita</code></strong>
94 (<span class="emphasis"><em>matita</em></span> is the default database name, you can
95 change it using the <em class="parameter"><code>db.user</code></em> key of the
96 configuration file). </p><p> Then you need to grant the necessary access permissions to the
97 database user of Matita, typing <strong class="userinput"><code>echo "grant all privileges
98 on matita.* to helm;" | mysql matita</code></strong> should do the trick
99 (<span class="emphasis"><em>helm</em></span> is the default user name used by Matita to
100 access the database, you can change it using the
101 <em class="parameter"><code>db.user</code></em> key of the configuration file).
102 </p><div class="note" style="margin-left: 0.5in; margin-right: 0.5in;"><h3 class="title">Note</h3><p> This way you create a database named <span class="emphasis"><em>matita</em></span>
103 on which anyone claiming to be the <span class="emphasis"><em>helm</em></span> user can
104 do everything (like adding dummy data or destroying the contained
105 one). It is strongly suggested to apply more fine grained permissions,
106 how to do it is out of the scope of this manual.</p></div></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="build_instructions"></a>Compiling and installing</h3></div></div></div><p> Once you get the source code the installations steps should be
107 quite familiar.</p><p> First of all you need to configure the build process executing
108 <strong class="userinput"><code>./configure</code></strong>. This will check that all needed
109 tools and library are installed and prepare the sources for compilation
110 and installation. </p><p> Quite a few (optional) arguments may be passed to the
111 <span class="application">configure</span> command line to change build time
112 parameters. They are listed below, together with their
113 default values: </p><div class="variablelist"><p class="title"><strong> <span class="application">configure</span> command line
114 arguments</strong></p><dl class="variablelist"><dt><span class="term">
115 <strong class="userinput"><code>--with-runtime-dir=<em class="replaceable"><code>dir</code></em></code></strong>
117 (<span class="emphasis"><em>Default:</em></span>
118 <code class="filename">/usr/local/matita</code>) Runtime base directory
119 where all Matita stuff (executables, configuration files,
120 standard library, ...) will be installed
121 </p></dd><dt><span class="term">
122 <strong class="userinput"><code>--with-dbhost=<em class="replaceable"><code>host</code></em></code></strong>
124 (<span class="emphasis"><em>Default:</em></span> localhost) Default SQL server
125 hostname. Will be used while building the standard library
126 during the installation and to create the default Matita
127 configuration. May be changed later in configuration file.
128 </p></dd><dt><span class="term">
129 <strong class="userinput"><code>--enable-debug</code></strong>
131 (<span class="emphasis"><em>Default:</em></span> disabled) Enable debugging code.
132 Not for the casual user.
133 </p></dd></dl></div><p> Then you will manage the build and install process using
134 <span class="application"><a class="ulink" href="http://www.gnu.org/software/make/" target="_top">make</a></span>
135 as usual. Below are reported the targets you have to invoke in sequence
136 to build and install:
137 </p><div class="variablelist"><p class="title"><strong><span class="application">make</span> targets</strong></p><dl class="variablelist"><dt><span class="term"><strong class="userinput"><code>world</code></strong></span></dt><dd><p>builds components needed by Matita and Matita itself
138 (in bytecode or native code depending
139 on the availability of the OCaml native code compiler) </p></dd><dt><span class="term"><strong class="userinput"><code>install</code></strong></span></dt><dd><p>installs Matita related tools, standard library and the
140 needed runtime stuff in the proper places on the filesystem.
141 </p><p>As a part of the installation process the Matita
142 standard library will be compiled, thus testing that the just
143 built <span class="application">matitac</span> compiler works
144 properly.</p><p>For this step you will need a working SQL database (for
145 indexing the standard library while you are compiling it). See
146 <a class="ulink" href="#database_setup" target="_top">Database setup</a>
147 for instructions on how to set it up.
148 </p></dd></dl></div></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_install.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_install.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="matita.conf.xml.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 2. Installation </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Configuring Matita</td></tr></table></div></body></html>