helm/www/matita/docs/manual-0.5.9/inst_from_src.html

   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&amp;path=%2F&amp;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.
  16
  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>
  19                   distribution,
  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.
  23           </p><p>
  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
  25           </p><p>
  26                   An official debian package is going to be added to the
  27                   archive too.
  28           </p></div><p>
  29
  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>
  34               </span>
  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
  37                   Expat</a> </span>
  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>
  41               </span>
  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
  45                   HTTP</a> </span>
  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>
  48               </span>
  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>
  52               </span>
  53             , </span><span class="term">
  54               <span class="application"> <a class="ulink" href="http://helm.cs.unibo.it/mml-widget/" target="_top">LablGtkMathView</a>
  55               </span>
  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>
  59               </span>
  60             , </span><span class="term">
  61               <span class="application"> <a class="ulink" href="http://helm.cs.unibo.it/software/lablgtksourceview/" target="_top">LablGtkSourceView</a>
  62               </span>
  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
  66                   MySQL</a> </span>
  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">
  72                 OCaml Sqlite3
  73               </a> </span>
  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>
  77               </span>
  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>
  81               </span>
  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>
  84               </span>
  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>
 116             </span></dt><dd><p>
 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>
 123             </span></dt><dd><p>
 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>
 130             </span></dt><dd><p>
 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>