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