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>(optional) &MYSQL; setup</title>
 251
 252       <para> To fully exploit &appname; indexing and search capabilities
 253         on a huge metadata set you may
 254         need a working &MYSQL; database. Detalied instructions on how to do
 255         it can be found in the <ulink type="http"
 256           url="http://dev.mysql.com/doc/">MySQL documentation</ulink>. Here you
 257         can find a quick howto. </para>
 258
 259       <para> In order to create a database you need administrator permissions on
 260         your MySQL installation, usually the root account has them. Once you
 261         have the permissions, a new database can be created executing
 262         <userinput>mysqladmin create matita</userinput>
 263         (<emphasis>matita</emphasis> is the default database name, you can
 264         change it using the <parameter>db.user</parameter> key of the
 265         configuration file). </para>
 266
 267       <para> Then you need to grant the necessary access permissions to the
 268         database user of &appname;, typing <userinput>echo "grant all privileges
 269           on matita.* to helm;" | mysql matita</userinput> should do the trick
 270         (<emphasis>helm</emphasis> is the default user name used by &appname; to
 271         access the database, you can change it using the
 272         <parameter>db.user</parameter> key of the configuration file).
 273       </para>
 274
 275       <note>
 276         <para> This way you create a database named <emphasis>matita</emphasis>
 277           on which anyone claiming to be the <emphasis>helm</emphasis> user can
 278           do everything (like adding dummy data or destroying the contained
 279           one). It is strongly suggested to apply more fine grained permissions,
 280           how to do it is out of the scope of this manual.</para>
 281       </note>
 282
 283     </sect2>
 284
 285     <sect2 id="build_instructions">
 286       <title>Compiling and installing</title>
 287
 288       <para> Once you get the source code the installations steps should be
 289         quite familiar.</para>
 290
 291       <para> First of all you need to configure the build process executing
 292         <userinput>./configure</userinput>. This will check that all needed
 293         tools and library are installed and prepare the sources for compilation
 294         and installation. </para>
 295
 296       <para> Quite a few (optional) arguments may be passed to the
 297         <application>configure</application> command line to change build time
 298         parameters. They are listed below, together with their
 299         default values: </para>
 300
 301         <variablelist>
 302           <title> <application>configure</application> command line
 303             arguments</title>
 304
 305           <varlistentry>
 306             <term>
 307               <userinput>--with-runtime-dir=<replaceable>dir</replaceable></userinput>
 308             </term>
 309             <listitem>
 310               <para>
 311                 (<emphasis>Default:</emphasis>
 312                 <filename>/usr/local/matita</filename>) Runtime base directory
 313                 where all &appname; stuff (executables, configuration files,
 314                 standard library, ...) will be installed
 315               </para>
 316             </listitem>
 317           </varlistentry>
 318
 319           <varlistentry>
 320             <term>
 321               <userinput>--with-dbhost=<replaceable>host</replaceable></userinput>
 322             </term>
 323             <listitem>
 324               <para>
 325                 (<emphasis>Default:</emphasis> localhost) Default SQL server
 326                 hostname. Will be used while building the standard library
 327                 during the installation and to create the default &appname;
 328                 configuration. May be changed later in configuration file.
 329               </para>
 330             </listitem>
 331           </varlistentry>
 332
 333           <varlistentry>
 334             <term>
 335               <userinput>--enable-debug</userinput>
 336             </term>
 337             <listitem>
 338               <para>
 339                 (<emphasis>Default:</emphasis> disabled) Enable debugging code.
 340                 Not for the casual user.
 341               </para>
 342             </listitem>
 343           </varlistentry>
 344         </variablelist>
 345
 346       <para> Then you will manage the build and install process using
 347         <application><ulink type="http"
 348             url="http://www.gnu.org/software/make/">make</ulink></application>
 349         as usual. Below are reported the targets you have to invoke in sequence
 350         to build and install:
 351       </para>
 352
 353         <variablelist>
 354           <title><application>make</application> targets</title>
 355
 356           <varlistentry>
 357             <term><userinput>world</userinput></term>
 358             <listitem>
 359               <para>builds components needed by &appname; and &appname; itself
 360                 (in bytecode or native code depending
 361                 on the availability of the OCaml native code compiler) </para>
 362             </listitem>
 363           </varlistentry>
 364
 365           <varlistentry>
 366             <term><userinput>install</userinput></term>
 367             <listitem>
 368               <para>installs &appname; related tools, standard library and the
 369                 needed runtime stuff in the proper places on the filesystem.
 370               </para>
 371               <para>As a part of the installation process the &appname;
 372                 standard library will be compiled, thus testing that the just
 373                 built <application>matitac</application> compiler works
 374                 properly.</para>
 375               <para>For this step you will need a working SQL database (for
 376                 indexing the standard library while you are compiling it). See
 377                 <ulink type="http" url="#database_setup">Database setup</ulink>
 378                 for instructions on how to set it up.
 379               </para>
 380             </listitem>
 381           </varlistentry>
 382
 383         </variablelist>
 384
 385     </sect2>
 386
 387   </sect1>
 388
 389   <sect1 id="matita.conf.xml">
 390     <title>Configuring &appname;</title>
 391     <para>
 392             The configuration file is divided in four sections. The user and
 393             matita ones are self explicative and does not need user
 394             intervention. Here we report a sample snippet for these two
 395             sections. The remaining db and getter sections will be explained in
 396             details later.
 397            <programlisting>
 398 <![CDATA[
 399   <section name="user">
 400     <key name="home">$(HOME)</key>
 401     <key name="name">$(USER)</key>
 402   </section>
 403   <section name="matita">
 404     <key name="basedir">$(user.home)/.matita</key>
 405     <key name="rt_base_dir">/usr/share/matita/</key>
 406     <key name="owner">$(user.name)</key>
 407   </section>
 408 ]]></programlisting>
 409     </para>
 410    <para>
 411            &appname; needs to store/fetch data and metadata. Data is essentially
 412            composed of XML files, metadata is a set of tuples for a relational
 413            model. Data and metadata can produced by the user or be already
 414            available. Both kind of data/metadata can be local and/or remote.
 415    </para>
 416    <para>
 417            The db section tells &appname; where to store and retrieve metadata,
 418            while the getter section describes where XML files have to be
 419            found. The following picture describes the suggested configuration.
 420            Dashed arrows are determined by the configuration file.
 421    </para>
 422    <figure><title>Configuring the Databases</title>
 423      <mediaobject>
 424        <imageobject>
 425          <imagedata fileref="figures/database.png" format="PNG" srccredit="Enrico Tassi"/>
 426        </imageobject>
 427        <textobject><phrase>How to configure the databases.</phrase></textobject>
 428      </mediaobject>
 429    </figure>
 430    <para>The getter</para>
 431    <para>
 432            Consider the following snippet and the URI
 433            <userinput>cic:/matita/foo/bar.con</userinput>. If &appname;
 434            is asked to read that object it will resolve the object trough
 435            the getter. Since the first two entries are equally specific
 436            (longest match rule applies) first the path
 437            <userinput>file://$(matita.rt_base_dir)/xml/standard-library/foo/bar.con</userinput>
 438            and then <userinput>file://$(user.home)/.matita/xml/matita/foo/bar.con</userinput>
 439            are inspected.
 440            <programlisting>
 441 <![CDATA[
 442   <section name="getter">
 443     <key name="cache_dir">$(user.home)/.matita/getter/cache</key>
 444     <key name="prefix">
 445       cic:/matita/
 446       file://$(matita.rt_base_dir)/xml/standard-library/
 447       ro
 448     </key>
 449     <key name="prefix">
 450       cic:/matita/
 451       file://$(user.home)/.matita/xml/matita/
 452     </key>
 453     <key name="prefix">
 454       cic:/Coq/
 455       http://mowgli.cs.unibo.it/xml/
 456       legacy
 457     </key>
 458   </section>
 459 ]]>
 460         </programlisting>
 461         if the same URI has to be written, the former prefix is skipped
 462         since it is marked as readonly (<userinput>ro</userinput>).
 463         Objects resolved using the third prefix are readonly too, and are
 464         retrieved using the network. There is no limit to the number of
 465         prefixes the user can define. The distinction between prefixes marked
 466         as readonly and legacy is that, legacy ones are really read only, while
 467         the ones marked with <userinput>ro</userinput> are considered for
 468         writing when &appname; is started in system mode (used to publish user
 469         developments in the library space).
 470    </para>
 471           <para>The db</para>
 472         <para>
 473            The database subsystem has three fron ends: library, user and
 474            legacy.  The latter is the only optional one. Every query is done on
 475            every frontend, making the duplicate free union of the results.
 476            The user front end kepps metadata produced by the user, and is thus
 477            heavily accessed in read/write mode, while the library and legacy
 478            fron ends are read only. Every front end can be connected to
 479            backend, the storage actually.
 480            Consider the following snippet.
 481            <programlisting>
 482 <![CDATA[
 483   <section name="db">
 484     <key name="metadata">mysql://mowgli.cs.unibo.it matita helm none legacy</key>
 485     <key name="metadata">file://$(matita.rt_base_dir) metadata.db helm helm library</key>
 486     <key name="metadata">file://$(matita.basedir) user.db helm helm user</key>
 487   </section>
 488 ]]>
 489         </programlisting>
 490         Here the usr database is a file (thus locally accessed trough the
 491         Sqlite library) placed in the user's home directory. The library one is
 492         placed in the &appname; runtime directory. The legacy fron end is
 493         connected to a remote &MYSQL; based storage. Every metadata key
 494         takes a path to the storage, the name of the database, the user name,
 495         a password (or <userinput>none</userinput>) and the name of the front
 496         end to which it is attached.
 497    </para>
 498   </sect1>
 499
 500 </chapter>
 501