helm/www/matita/docs/manual/sec_install.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">
   3 <html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Chapter 2. Installation</title><link rel="stylesheet" href="docbook.css" type="text/css" /><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0&#10; User Manual (rev. 1α)" /><link rel="up" href="index.html" title="Matita V0.1.0&#10; User Manual (rev. 1α)" /><link rel="prev" href="WrtCoq.html" title="Matita vs Coq" /><link rel="next" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /></head><body><a xmlns="" href="../../"><div class="matita_logo"><img src="../../images/matita-tiny.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">Chapter 2. Installation</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="WrtCoq.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_gettingstarted.html">Next</a></td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_install"></a>Chapter 2. Installation</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_install.html#inst_from_src">Installing from sources</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_install.html#get_source_code">Getting the source code</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_requirements">Requirements</a></span></dt><dt><span class="sect2"><a href="sec_install.html#database_setup">Database setup</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_instructions">Compiling and installing</a></span></dt></dl></dd></dl></div><div class="sect1" lang="en" xml:lang="en"><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>Currently, the only intended way to install Matita is starting
   4       from its source code.  </p><div class="sect2" lang="en" xml:lang="en"><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:
   5         </p><div class="orderedlist"><ol type="1"><li><p> go to the <a href="http://matita.cs.unibo.it/download.shtml" target="_top">download
   6                 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></li><li><p> get the development sources from <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2F&amp;sc=0" target="_top">our
   7                 SVN repository</a>. You will need the
   8               <span class="application">components/</span> and
   9               <span class="application">matita/</span> directories from the
  10               <code class="filename">trunk/helm/software/</code> directory, plus the
  11               <code class="filename">configure</code> and <code class="filename">Makefile*</code>
  12               stuff from the same directory.  </p><p>In this case you will need to run
  13                 <span><strong class="command">autoconf</strong></span> before proceding with the building
  14                 instructions below.</p></li></ol></div><p>
  15       </p></div><div class="sect2" lang="en" xml:lang="en"><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
  16         tools and libraries. They are listed below.
  17
  18         </p><div class="note" style="margin-left: 0.5in; margin-right: 0.5in;"><h3 class="title">Note for Debian users</h3><p>If you are running a <a href="http://www.debian.org" target="_top">Debian GNU/Linux</a> distribution
  19             you can have APT install all the required tools and libraries by
  20             adding the following repository to your
  21             <code class="filename">/etc/apt/sources.list</code>: </p><pre class="programlisting">
  22               deb <a href="http://people.debian.org/~zack" target="_top">http://people.debian.org/~zack</a> unstable helm
  23           </pre><p> and installing the
  24           <span class="application">helm-matita-deps</span> package.</p></div><p>
  25
  26         </p><div class="variablelist"><p class="title"><b>Required tools and libraries</b></p><dl><dt><span class="term">
  27               <span class="application"> <a href="http://caml.inria.fr" target="_top">OCaml</a> </span>
  28             </span></dt><dd><p> the Objective Caml compiler, version 3.09 or above </p></dd><dt><span class="term">
  29               <span class="application"> <a href="http://www.ocaml-programming.de/packages/" target="_top">Findlib</a>
  30               </span>
  31             </span></dt><dd><p> OCaml package manager, version 1.1.1 or above</p></dd><dt><span class="term">
  32               <span class="application"> <a href="http://www.xs4all.nl/~mmzeeman/ocaml/" target="_top">OCaml
  33                   Expat</a> </span>
  34             </span></dt><dd><p>OCaml bindings for the <span class="application"><a href="http://expat.sourceforge.net/" target="_top">expat</a>
  35                   library</span> </p></dd><dt><span class="term">
  36               <span class="application"> <a href="http://gmetadom.sourceforge.net/" target="_top">GMetaDOM</a>
  37               </span>
  38             </span></dt><dd><p>OCaml bindings for the <span class="application"><a href="http://gdome2.cs.unibo.it/" target="_top">Gdome 2</a>
  39                   library</span></p></dd><dt><span class="term">
  40               <span class="application"> <a href="http://www.bononia.it/~zack/ocaml-http.en.html" target="_top">OCaml
  41                   HTTP</a> </span>
  42             </span></dt><dd><p> OCaml library to write HTTP daemons (and clients) </p></dd><dt><span class="term">
  43               <span class="application"> <a href="http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html" target="_top">LablGTK</a>
  44               </span>
  45             </span></dt><dd><p> OCaml bindings for the <span class="application"> <a href="http://www.gtk.org" target="_top"> GTK+</a> library
  46               </span>, version 2.6.0 or above </p></dd><dt><span class="term">
  47               <span class="application"> <a href="http://helm.cs.unibo.it/mml-widget/" target="_top">GtkMathView</a>
  48               </span>
  49             , </span><span class="term">
  50               <span class="application"> <a href="http://helm.cs.unibo.it/mml-widget/" target="_top">LablGtkMathView</a>
  51               </span>
  52             </span></dt><dd><p> GTK+ widget to render <a href="http://www.w3.org/Math/" target="_top">MathML</a> documents and its
  53                 OCaml bindings </p></dd><dt><span class="term">
  54               <span class="application"> <a href="http://gtksourceview.sourceforge.net/" target="_top">GtkSourceView</a>
  55               </span>
  56             , </span><span class="term">
  57               <span class="application"> <a href="http://helm.cs.unibo.it/software/lablgtksourceview/" target="_top">LablGtkSourceView</a>
  58               </span>
  59             </span></dt><dd><p> extension for the GTK+ text widget (adding the typical
  60                 features of source code editors) and its OCaml bindings </p></dd><dt><span class="term"> <span class="application"> <a href="http://www.mysql.com" target="_top">MySQL</a> </span> , </span><span class="term">
  61               <span class="application"> <a href="http://raevnos.pennmush.org/code/ocaml-mysql/" target="_top">OCaml
  62                   MySQL</a> </span>
  63             </span></dt><dd><p> SQL database and OCaml bindings for its client-side library
  64               </p><p> The SQL database itself is not strictly needed to run
  65                 Matita, but we stronly encourage its use since a lot of
  66                 features are disabled without it. Still, the OCaml bindings of
  67                 the library are needed at compile time.</p></dd><dt><span class="term">
  68               <span class="application"> <a href="http://ocamlnet.sourceforge.net/" target="_top">Ocamlnet</a>
  69               </span>
  70             </span></dt><dd><p> collection of OCaml libraries to deal with
  71                 application-level Internet protocols and conventions </p></dd><dt><span class="term">
  72               <span class="application"> <a href="http://www.cduce.org/download.html" target="_top">ulex</a>
  73               </span>
  74             </span></dt><dd><p> Unicode lexer generator for OCaml </p></dd><dt><span class="term">
  75               <span class="application"> <a href="http://cristal.inria.fr/~xleroy/software.html" target="_top">CamlZip</a>
  76               </span>
  77             </span></dt><dd><p> OCaml library to access <code class="filename">.gz</code> files
  78               </p></dd></dl></div><p> </p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="database_setup"></a>Database setup</h3></div></div></div><p> To fully exploit Matita indexing and search capabilities you
  79         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
  80         it can be found in the <a href="http://dev.mysql.com/doc/" target="_top">MySQL documentation</a>. Here you
  81         can find a quick howto. </p><p> In order to create a database you need administrator permissions on
  82         your MySQL installation, usually the root account has them. Once you
  83         have the permissions, a new database can be created executing
  84         <strong class="userinput"><code>mysqladmin create matita</code></strong>
  85         (<span class="emphasis"><em>matita</em></span> is the default database name, you can
  86         change it using the <em class="parameter"><code>db.user</code></em> key of the
  87         configuration file). </p><p> Then you need to grant the necessary access permissions to the
  88         database user of Matita, typing <strong class="userinput"><code>echo "grant all privileges
  89           on matita.* to helm;" | mysql matita</code></strong> should do the trick
  90         (<span class="emphasis"><em>helm</em></span> is the default user name used by Matita to
  91         access the database, you can change it using the
  92         <em class="parameter"><code>db.user</code></em> key of the configuration file).
  93       </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>
  94           on which anyone claiming to be the <span class="emphasis"><em>helm</em></span> user can
  95           do everything (like adding dummy data or destroying the contained
  96           one). It is strongly suggested to apply more fine grained permissions,
  97           how to do it is out of the scope of this manual.</p></div></div><div class="sect2" lang="en" xml:lang="en"><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
  98         quite familiar.</p><p> First of all you need to configure the build process executing
  99         <strong class="userinput"><code>./configure</code></strong>. This will check that all needed
 100         tools and library are installed and prepare the sources for compilation
 101         and installation. </p><p> Quite a few (optional) arguments may be passed to the
 102         <span class="application">configure</span> command line to change build time
 103         parameters. They are listed in the table below, together with their
 104         default values.
 105
 106         </p><div class="table"><a id="id2519563"></a><p class="title"><b>Table 2.1.  <span class="application">configure</span> command line
 107             arguments</b></p><table summary=" configure command line&#10;&#9;    arguments" border="1"><colgroup><col /><col /><col /></colgroup><thead><tr><th align="center">Argument</th><th align="center">Default</th><th align="center">Description</th></tr></thead><tbody><tr><td align="left">
 108                   <strong class="userinput"><code>--with-runtime-dir=<em class="replaceable"><code>dir</code></em></code></strong>
 109                 </td><td align="left"> <code class="filename">/usr/local/matita/</code> </td><td align="left"> <p> Runtime base directory where all Matita stuff
 110                     (executables, configuration files, standard
 111                     library, ...) will be installed </p> </td></tr><tr><td align="left">
 112                   <strong class="userinput"><code>--with-dbhost=<em class="replaceable"><code>host</code></em></code></strong>
 113                 </td><td align="left"> localhost </td><td align="left"> <p>Default SQL server hostname. Will be used while
 114                     building the standard library during the installation and to
 115                     create the default Matita configuration. May be changed
 116                     later in configuration file.</p></td></tr><tr><td align="left"> <strong class="userinput"><code>--enable-debug</code></strong></td><td align="left"> disabled </td><td align="left"> <p> Enable debugging code. Not for the casual user.
 117                   </p> </td></tr></tbody></table></div><p>
 118
 119       </p><p> Then you will manage the build and install process using
 120         <span class="application"><a href="http://www.gnu.org/software/make/" target="_top">make</a></span>
 121         as usual. Below are reported the targets you have to invoke in sequence
 122         to build and install.
 123
 124         </p><div class="variablelist"><p class="title"><b><span class="application">make</span> targets</b></p><dl><dt><span class="term"><strong class="userinput"><code>world</code></strong></span></dt><dd><p>builds components needed by Matita and Matita itself
 125                 (in bytecode or native code depending
 126                 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
 127                 needed runtime stuff in the proper places on the filesystem.
 128               </p><p>As a part of the installation process the Matita
 129                 standard library will be compiled, thus testing that the just
 130                 built <span class="application">matitac</span> compiler works
 131                 properly.</p><p>For this step you will need a working SQL database (for
 132                 indexing the standard library while you are compiling it). See
 133                 <a href="#database_setup" target="_top">Database setup</a>
 134                 for instructions on how to set it up.
 135               </p></dd></dl></div><p>
 136
 137       </p></div></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="WrtCoq.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="sec_gettingstarted.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Matita vs Coq </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 3. Getting started</td></tr></table></div></body></html>