matita/help/C/sec_install.xml

   1
   2 <!-- ============= Installation ============================== -->
   3
   4 <chapter id="sec_install">
   5   <title>Installation</title>
   6
   7   <sect1 id="inst_from_src">
   8     <title>Installing from sources</title>
   9
  10     <para>Currently, the only intended way to install &appname; is starting
  11       from its source code.  </para>
  12
  13     <sect2 id="get_source_code">
  14       <title>Getting the source code</title>
  15
  16       <para>You can get the &appname; source code in two ways:
  17         <orderedlist>
  18
  19           <listitem> <para> go to the <ulink type="http"
  20                 url="http://matita.cs.unibo.it/download.shtml">download
  21                 page</ulink> and get the <ulink type="http"
  22                 url="http://matita.cs.unibo.it/sources/matita-latest.tar.gz"
  23                 >latest released source tarball</ulink>;</para> </listitem>
  24
  25           <listitem> <para> get the development sources from <ulink type="http"
  26                 url="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2F&amp;sc=0">our
  27                 SVN repository</ulink>. You will need the
  28               <application>components/</application> and
  29               <application>matita/</application> directories from the
  30               <filename>trunk/helm/software/</filename> directory, plus the
  31               <filename>configure</filename> and <filename>Makefile*</filename>
  32               stuff from the same directory.  </para>
  33
  34               <para>In this case you will need to run
  35                 <command>autoconf</command> before proceding with the building
  36                 instructions below.</para> </listitem>
  37
  38         </orderedlist>
  39       </para>
  40
  41     </sect2>
  42
  43     <sect2 id="build_requirements">
  44       <title>Requirements</title>
  45
  46       <para>In order to build &appname; from sources you will need some
  47         tools and libraries. They are listed below.
  48
  49         <note>
  50           <title>Note for Debian users</title>
  51
  52           <para>If you are running a <ulink type="http"
  53               url="http://www.debian.org">Debian GNU/Linux</ulink> distribution
  54             you can have APT install all the required tools and libraries by
  55             adding the following repository to your
  56             <filename>/etc/apt/sources.list</filename>: <programlisting>
  57               deb <ulink type="http"
  58                 url="http://people.debian.org/~zack">http://people.debian.org/~zack</ulink> unstable helm
  59           </programlisting> and installing the
  60           <application>helm-matita-deps</application> package.</para>
  61
  62         </note>
  63
  64         <variablelist>
  65           <title>Required tools and libraries</title>
  66
  67           <varlistentry>
  68             <term>
  69               <application> <ulink type="http"
  70                   url="http://caml.inria.fr">OCaml</ulink> </application>
  71             </term>
  72             <listitem>
  73               <para> the Objective Caml compiler, version 3.09 or above </para>
  74             </listitem>
  75           </varlistentry>
  76
  77           <varlistentry>
  78             <term>
  79               <application> <ulink type="http"
  80                   url="http://www.ocaml-programming.de/packages/">Findlib</ulink>
  81               </application>
  82             </term>
  83             <listitem>
  84               <para> OCaml package manager, version 1.1.1 or above</para>
  85             </listitem>
  86           </varlistentry>
  87
  88           <varlistentry>
  89             <term>
  90               <application> <ulink type="http"
  91                   url="http://www.xs4all.nl/~mmzeeman/ocaml/">OCaml
  92                   Expat</ulink> </application>
  93             </term>
  94             <listitem>
  95               <para>OCaml bindings for the <application><ulink type="http"
  96                     url="http://expat.sourceforge.net/">expat</ulink>
  97                   library</application> </para>
  98             </listitem>
  99           </varlistentry>
 100
 101           <varlistentry>
 102             <term>
 103               <application> <ulink type="http"
 104                   url="http://gmetadom.sourceforge.net/">GMetaDOM</ulink>
 105               </application>
 106             </term>
 107             <listitem>
 108               <para>OCaml bindings for the <application><ulink type="http"
 109                     url="http://gdome2.cs.unibo.it/">Gdome 2</ulink>
 110                   library</application></para>
 111             </listitem>
 112           </varlistentry>
 113
 114           <varlistentry>
 115             <term>
 116               <application> <ulink type="http"
 117                   url="http://www.bononia.it/~zack/ocaml-http.en.html">OCaml
 118                   HTTP</ulink> </application>
 119             </term>
 120             <listitem>
 121               <para> OCaml library to write HTTP daemons (and clients) </para>
 122             </listitem>
 123           </varlistentry>
 124
 125           <varlistentry>
 126             <term>
 127               <application> <ulink type="http"
 128                   url="http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html">LablGTK</ulink>
 129               </application>
 130             </term>
 131             <listitem>
 132               <para> OCaml bindings for the <application> <ulink type="http"
 133                     url="http://www.gtk.org"> GTK+</ulink> library
 134               </application>, version 2.6.0 or above </para>
 135             </listitem>
 136           </varlistentry>
 137
 138           <varlistentry>
 139             <term>
 140               <application> <ulink type="http"
 141                   url="http://helm.cs.unibo.it/mml-widget/">GtkMathView</ulink>
 142               </application>
 143             </term>
 144             <term>
 145               <application> <ulink type="http"
 146                   url="http://helm.cs.unibo.it/mml-widget/">LablGtkMathView</ulink>
 147               </application>
 148             </term>
 149             <listitem>
 150               <para> GTK+ widget to render <ulink type="http"
 151                   url="http://www.w3.org/Math/">MathML</ulink> documents and its
 152                 OCaml bindings </para>
 153             </listitem>
 154           </varlistentry>
 155
 156           <varlistentry>
 157             <term>
 158               <application> <ulink type="http"
 159                   url="http://gtksourceview.sourceforge.net/">GtkSourceView</ulink>
 160               </application>
 161             </term>
 162             <term>
 163               <application> <ulink type="http"
 164                   url="http://helm.cs.unibo.it/software/lablgtksourceview/">LablGtkSourceView</ulink>
 165               </application>
 166             </term>
 167             <listitem>
 168               <para> extension for the GTK+ text widget (adding the typical
 169                 features of source code editors) and its OCaml bindings </para>
 170             </listitem>
 171           </varlistentry>
 172
 173           <varlistentry>
 174             <term> &MYSQL; </term>
 175             <term>
 176               <application> <ulink type="http"
 177                   url="http://raevnos.pennmush.org/code/ocaml-mysql/">OCaml
 178                   MySQL</ulink> </application>
 179             </term>
 180             <listitem>
 181               <para> SQL database and OCaml bindings for its client-side library
 182               </para>
 183               <para> The SQL database itself is not strictly needed to run
 184                 &appname;, but we stronly encourage its use since a lot of
 185                 features are disabled without it. Still, the OCaml bindings of
 186                 the library are needed at compile time.</para>
 187             </listitem>
 188           </varlistentry>
 189
 190           <varlistentry>
 191             <term>
 192               <application> <ulink type="http"
 193                   url="http://ocamlnet.sourceforge.net/">Ocamlnet</ulink>
 194               </application>
 195             </term>
 196             <listitem>
 197               <para> collection of OCaml libraries to deal with
 198                 application-level Internet protocols and conventions </para>
 199             </listitem>
 200           </varlistentry>
 201
 202           <varlistentry>
 203             <term>
 204               <application> <ulink type="http"
 205                   url="http://www.cduce.org/download.html">ulex</ulink>
 206               </application>
 207             </term>
 208             <listitem>
 209               <para> Unicode lexer generator for OCaml </para>
 210             </listitem>
 211           </varlistentry>
 212
 213           <varlistentry>
 214             <term>
 215               <application> <ulink type="http"
 216                   url="http://cristal.inria.fr/~xleroy/software.html">CamlZip</ulink>
 217               </application>
 218             </term>
 219             <listitem>
 220               <para> OCaml library to access <filename>.gz</filename> files
 221               </para>
 222             </listitem>
 223           </varlistentry>
 224
 225         </variablelist> </para>
 226
 227     </sect2>
 228
 229     <sect2 id="database_setup">
 230       <title>Database setup</title>
 231
 232       <para> To fully exploit &appname; indexing and search capabilities you
 233         will need a working &MYSQL; database. Detalied instructions on how to do
 234         it can be found in the <ulink type="http"
 235           url="http://dev.mysql.com/doc/">MySQL documentation</ulink>. Here you
 236         can find a quick howto. </para>
 237
 238       <para> In order to create a database you need administrator permissions on
 239         your MySQL installation, usually the root account has them. Once you
 240         have the permissions, a new database can be created executing
 241         <userinput>mysqladmin create matita</userinput>
 242         (<emphasis>matita</emphasis> is the default database name, you can
 243         change it using the <parameter>db.user</parameter> key of the
 244         configuration file). </para>
 245
 246       <para> Then you need to grant the necessary access permissions to the
 247         database user of &appname;, typing <userinput>echo "grant all privileges
 248           on matita.* to helm;" | mysql matita</userinput> should do the trick
 249         (<emphasis>helm</emphasis> is the default user name used by &appname; to
 250         access the database, you can change it using the
 251         <parameter>db.user</parameter> key of the configuration file).
 252       </para>
 253
 254       <note>
 255         <para> This way you create a database named <emphasis>matita</emphasis>
 256           on which anyone claiming to be the <emphasis>helm</emphasis> user can
 257           do everything (like adding dummy data or destroying the contained
 258           one). It is strongly suggested to apply more fine grained permissions,
 259           how to do it is out of the scope of this manual.</para>
 260       </note>
 261
 262     </sect2>
 263
 264     <sect2 id="build_instructions">
 265       <title>Compiling and installing</title>
 266
 267       <para> Once you get the source code the installations steps should be
 268         quite familiar.</para>
 269
 270       <para> First of all you need to configure the build process executing
 271         <userinput>./configure</userinput>. This will check that all needed
 272         tools and library are installed and prepare the sources for compilation
 273         and installation. </para>
 274
 275       <para> Quite a few (optional) arguments may be passed to the
 276         <application>configure</application> command line to change build time
 277         parameters. They are listed below, together with their
 278         default values: </para>
 279
 280         <variablelist>
 281           <title> <application>configure</application> command line
 282             arguments</title>
 283
 284           <varlistentry>
 285             <term>
 286               <userinput>--with-runtime-dir=<replaceable>dir</replaceable></userinput>
 287             </term>
 288             <listitem>
 289               <para>
 290                 (<emphasis>Default:</emphasis>
 291                 <filename>/usr/local/matita</filename>) Runtime base directory
 292                 where all &appname; stuff (executables, configuration files,
 293                 standard library, ...) will be installed
 294               </para>
 295             </listitem>
 296           </varlistentry>
 297
 298           <varlistentry>
 299             <term>
 300               <userinput>--with-dbhost=<replaceable>host</replaceable></userinput>
 301             </term>
 302             <listitem>
 303               <para>
 304                 (<emphasis>Default:</emphasis> localhost) Default SQL server
 305                 hostname. Will be used while building the standard library
 306                 during the installation and to create the default &appname;
 307                 configuration. May be changed later in configuration file.
 308               </para>
 309             </listitem>
 310           </varlistentry>
 311
 312           <varlistentry>
 313             <term>
 314               <userinput>--enable-debug</userinput>
 315             </term>
 316             <listitem>
 317               <para>
 318                 (<emphasis>Default:</emphasis> disabled) Enable debugging code.
 319                 Not for the casual user.
 320               </para>
 321             </listitem>
 322           </varlistentry>
 323         </variablelist>
 324
 325       <para> Then you will manage the build and install process using
 326         <application><ulink type="http"
 327             url="http://www.gnu.org/software/make/">make</ulink></application>
 328         as usual. Below are reported the targets you have to invoke in sequence
 329         to build and install:
 330       </para>
 331
 332         <variablelist>
 333           <title><application>make</application> targets</title>
 334
 335           <varlistentry>
 336             <term><userinput>world</userinput></term>
 337             <listitem>
 338               <para>builds components needed by &appname; and &appname; itself
 339                 (in bytecode or native code depending
 340                 on the availability of the OCaml native code compiler) </para>
 341             </listitem>
 342           </varlistentry>
 343
 344           <varlistentry>
 345             <term><userinput>install</userinput></term>
 346             <listitem>
 347               <para>installs &appname; related tools, standard library and the
 348                 needed runtime stuff in the proper places on the filesystem.
 349               </para>
 350               <para>As a part of the installation process the &appname;
 351                 standard library will be compiled, thus testing that the just
 352                 built <application>matitac</application> compiler works
 353                 properly.</para>
 354               <para>For this step you will need a working SQL database (for
 355                 indexing the standard library while you are compiling it). See
 356                 <ulink type="http" url="#database_setup">Database setup</ulink>
 357                 for instructions on how to set it up.
 358               </para>
 359             </listitem>
 360           </varlistentry>
 361
 362         </variablelist>
 363
 364     </sect2>
 365
 366   </sect1>
 367
 368   <sect1 id="matita.conf.xml">
 369     <title>Configuring Matita</title>
 370     <para>
 371     The file <emphasis>matita.conf.xml</emphasis>...
 372     &TODO;
 373     </para>
 374    <figure><title>Configuring the Databases</title>
 375      <mediaobject>
 376        <imageobject>
 377          <imagedata fileref="figures/database.png" format="PNG" srccredit="Enrico Tassi"/>
 378        </imageobject>
 379        <textobject><phrase>How to configure the databases.</phrase></textobject>
 380      </mediaobject>
 381    </figure>
 382   </sect1>
 383
 384 </chapter>
 385