helm/software/matita/help/C/sec_install.xml

   1
   2 <!-- ============= Installation ============================== -->
   3
   4 <chapter id="sec_install">
   5   <title>Installation</title>
   6
   7   <para>
   8           &appname; is a quite complex piece of software, we thus recommend
   9           you to either install al precompiled version or use the LiveCD.
  10           If you are running Debian GNU/Linux (or one of its derivatives
  11           like Ubuntu), you can install matita typing
  12            <programlisting><![CDATA[ aptitude install matita matita-standard-library ]]></programlisting>
  13           If you are running MacOSX or Windows, give the LiveCD a try before
  14           trying to compile &appname; from its sources.
  15   </para>
  16
  17   <sect1 id="inst_livecd">
  18     <title>Using the LiveCD</title>
  19
  20     <para>
  21             In the following, we will assume you have installed
  22             <ulink type="http" url="http://www.virtualbox.org">virtualbox</ulink>
  23             for your platform and downloaded the .iso image of the LiveCD
  24     </para>
  25
  26     <sect2 id="make_vmachine">
  27             <title>Creating the virtual machine</title>
  28     <para>
  29             Click on the New button, a wizard will popup, you should ask to
  30             its questions as follows
  31       <orderedlist>
  32               <listitem><para>
  33                 The name should be something like &appname;, but can
  34                 be any meaningful string.
  35               </para></listitem>
  36               <listitem><para>
  37                 The OS type should be Debian
  38               </para></listitem>
  39               <listitem><para>
  40                 The base memory size can be 256 mega bytes, but you may
  41                 want to increase it if you are going to work with huge
  42                 formalizations.
  43              </para></listitem>
  44           <listitem><para>
  45          The boot hard disk should be no hard disk. It may complain
  46          that this choice is not common, but it is right, since you
  47          will run a LiveCD you do not need to emulate an hard drive.
  48           </para></listitem>
  49       </orderedlist>
  50       Now that you are done with the creation of the virtual machine,
  51       you need to insert the LiveCD in the virtual cd reader unit.
  52       </para>
  53    <figure><title>The brand new virtual machine</title>
  54      <mediaobject>
  55        <imageobject>
  56          <imagedata fileref="figures/vbox1.png" format="PNG" srccredit="Enrico Tassi"/>
  57        </imageobject>
  58        <textobject><phrase>The breand new virtual machine</phrase></textobject>
  59      </mediaobject>
  60    </figure>
  61    <para>
  62       Click on CD/DVD-ROM (that should display something like: Not mouted).
  63       Then click on mount CD/DVD drive and select the ISO image
  64       option. The combo-box should display no available image, you need to
  65       add the ISO image you downloaded from the &appname; website clicking on
  66       the button near the combo-box.
  67       to start the virtual machine.
  68     </para>
  69    <figure><title>Mounting an ISO image</title>
  70      <mediaobject>
  71        <imageobject>
  72          <imagedata fileref="figures/vbox2.png" format="PNG" srccredit="Enrico Tassi"/>
  73        </imageobject>
  74        <textobject><phrase>Mounting an ISO image</phrase></textobject>
  75      </mediaobject>
  76    </figure>
  77    <para>
  78       In the newely opened window click
  79       the Add button, choose the file you downloaded
  80       (usually matita-version.iso) and select that entry.
  81     </para>
  82    <figure><title>Choosing the ISO image</title>
  83      <mediaobject>
  84        <imageobject>
  85          <imagedata fileref="figures/vbox3.png" format="PNG" srccredit="Enrico Tassi"/>
  86        </imageobject>
  87        <textobject><phrase>Choosing the ISO image</phrase></textobject>
  88      </mediaobject>
  89    </figure>
  90    <para>
  91       You are now ready
  92       to start the virtual machine.
  93     </para>
  94     </sect2>
  95     <sect2>
  96             <title>Sharing files with the real PC</title>
  97             TODO
  98     </sect2>
  99
 100   </sect1>
 101
 102   <sect1 id="inst_from_src">
 103     <title>Installing from sources</title>
 104
 105     <para>Install &appname; from the sources is hard, you have been warned!
 106     </para>
 107
 108     <sect2 id="get_source_code">
 109       <title>Getting the source code</title>
 110
 111       <para>You can get the &appname; source code in two ways:
 112         <orderedlist>
 113
 114           <listitem> <para> go to the <ulink type="http"
 115                 url="http://matita.cs.unibo.it/download.shtml">download
 116                 page</ulink> and get the <ulink type="http"
 117                 url="http://matita.cs.unibo.it/sources/matita-latest.tar.gz"
 118                 >latest released source tarball</ulink>;</para> </listitem>
 119
 120           <listitem> <para> get the development sources from <ulink type="http"
 121                 url="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2F&amp;sc=0">our
 122                 SVN repository</ulink>. You will need the
 123               <application>components/</application> and
 124               <application>matita/</application> directories from the
 125               <filename>trunk/helm/software/</filename> directory, plus the
 126               <filename>configure</filename> and <filename>Makefile*</filename>
 127               stuff from the same directory.  </para>
 128
 129               <para>In this case you will need to run
 130                 <command>autoconf</command> before proceding with the building
 131                 instructions below.</para> </listitem>
 132
 133         </orderedlist>
 134       </para>
 135
 136     </sect2>
 137
 138     <sect2 id="build_requirements">
 139       <title>Requirements</title>
 140
 141       <para>In order to build &appname; from sources you will need some
 142         tools and libraries. They are listed below.
 143
 144         <note>
 145           <title>Note for Debian (and derivatives) users</title>
 146
 147           <para>If you are running a
 148                   <ulink type="http"
 149                           url="http://www.debian.org">Debian GNU/Linux</ulink>
 150                   distribution,
 151                   or any of its derivative like <ulink type="http"
 152                           url="http://ubuntu.com">Ubuntu</ulink>,
 153                   you can use APT to install all the required tools and
 154                   libraries since they are all part of the Debian archive.
 155           </para>
 156           <para>
 157                   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
 158           </para>
 159           <para>
 160                   An official debian package is going to be added to the
 161                   archive too.
 162           </para>
 163
 164         </note>
 165
 166         <variablelist>
 167           <title>Required tools and libraries</title>
 168
 169           <varlistentry>
 170             <term>
 171               <application> <ulink type="http"
 172                   url="http://caml.inria.fr">OCaml</ulink> </application>
 173             </term>
 174             <listitem>
 175               <para> the Objective Caml compiler, version 3.09 or above </para>
 176             </listitem>
 177           </varlistentry>
 178
 179           <varlistentry>
 180             <term>
 181               <application> <ulink type="http"
 182                   url="http://www.ocaml-programming.de/packages/">Findlib</ulink>
 183               </application>
 184             </term>
 185             <listitem>
 186               <para> OCaml package manager, version 1.1.1 or above</para>
 187             </listitem>
 188           </varlistentry>
 189
 190           <varlistentry>
 191             <term>
 192               <application> <ulink type="http"
 193                   url="http://www.xs4all.nl/~mmzeeman/ocaml/">OCaml
 194                   Expat</ulink> </application>
 195             </term>
 196             <listitem>
 197               <para>OCaml bindings for the <application><ulink type="http"
 198                     url="http://expat.sourceforge.net/">expat</ulink>
 199                   library</application> </para>
 200             </listitem>
 201           </varlistentry>
 202
 203           <varlistentry>
 204             <term>
 205               <application> <ulink type="http"
 206                   url="http://gmetadom.sourceforge.net/">GMetaDOM</ulink>
 207               </application>
 208             </term>
 209             <listitem>
 210               <para>OCaml bindings for the <application><ulink type="http"
 211                     url="http://gdome2.cs.unibo.it/">Gdome 2</ulink>
 212                   library</application></para>
 213             </listitem>
 214           </varlistentry>
 215
 216           <varlistentry>
 217             <term>
 218               <application> <ulink type="http"
 219                   url="http://www.bononia.it/~zack/ocaml-http.en.html">OCaml
 220                   HTTP</ulink> </application>
 221             </term>
 222             <listitem>
 223               <para> OCaml library to write HTTP daemons (and clients) </para>
 224             </listitem>
 225           </varlistentry>
 226
 227           <varlistentry>
 228             <term>
 229               <application> <ulink type="http"
 230                   url="http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html">LablGTK</ulink>
 231               </application>
 232             </term>
 233             <listitem>
 234               <para> OCaml bindings for the <application> <ulink type="http"
 235                     url="http://www.gtk.org"> GTK+</ulink> library
 236               </application>, version 2.6.0 or above </para>
 237             </listitem>
 238           </varlistentry>
 239
 240           <varlistentry>
 241             <term>
 242               <application> <ulink type="http"
 243                   url="http://helm.cs.unibo.it/mml-widget/">GtkMathView</ulink>
 244               </application>
 245             </term>
 246             <term>
 247               <application> <ulink type="http"
 248                   url="http://helm.cs.unibo.it/mml-widget/">LablGtkMathView</ulink>
 249               </application>
 250             </term>
 251             <listitem>
 252               <para> GTK+ widget to render <ulink type="http"
 253                   url="http://www.w3.org/Math/">MathML</ulink> documents and its
 254                 OCaml bindings </para>
 255             </listitem>
 256           </varlistentry>
 257
 258           <varlistentry>
 259             <term>
 260               <application> <ulink type="http"
 261                   url="http://gtksourceview.sourceforge.net/">GtkSourceView</ulink>
 262               </application>
 263             </term>
 264             <term>
 265               <application> <ulink type="http"
 266                   url="http://helm.cs.unibo.it/software/lablgtksourceview/">LablGtkSourceView</ulink>
 267               </application>
 268             </term>
 269             <listitem>
 270               <para> extension for the GTK+ text widget (adding the typical
 271                 features of source code editors) and its OCaml bindings </para>
 272             </listitem>
 273           </varlistentry>
 274
 275           <varlistentry>
 276             <term> &MYSQL; </term>
 277             <term>
 278               <application> <ulink type="http"
 279                   url="http://raevnos.pennmush.org/code/ocaml-mysql/">OCaml
 280                   MySQL</ulink> </application>
 281             </term>
 282             <listitem>
 283               <para> SQL database and OCaml bindings for its client-side library
 284               </para>
 285               <para> The SQL database itself is not strictly needed to run
 286                 &appname;, but the client libraries are.</para>
 287             </listitem>
 288           </varlistentry>
 289
 290           <varlistentry>
 291             <term> &Sqlite; </term>
 292             <term>
 293                     <application>
 294                           <ulink type="http"
 295                               url="http://ocaml.info/home/ocaml_sources.html">
 296                 OCaml Sqlite3
 297               </ulink> </application>
 298             </term>
 299             <listitem>
 300               <para> Sqlite database and OCaml bindings
 301               </para>
 302             </listitem>
 303           </varlistentry>
 304
 305           <varlistentry>
 306             <term>
 307               <application> <ulink type="http"
 308                   url="http://ocamlnet.sourceforge.net/">Ocamlnet</ulink>
 309               </application>
 310             </term>
 311             <listitem>
 312               <para> collection of OCaml libraries to deal with
 313                 application-level Internet protocols and conventions </para>
 314             </listitem>
 315           </varlistentry>
 316
 317           <varlistentry>
 318             <term>
 319               <application> <ulink type="http"
 320                   url="http://www.cduce.org/download.html">ulex</ulink>
 321               </application>
 322             </term>
 323             <listitem>
 324               <para> Unicode lexer generator for OCaml </para>
 325             </listitem>
 326           </varlistentry>
 327
 328           <varlistentry>
 329             <term>
 330               <application> <ulink type="http"
 331                   url="http://cristal.inria.fr/~xleroy/software.html">CamlZip</ulink>
 332               </application>
 333             </term>
 334             <listitem>
 335               <para> OCaml library to access <filename>.gz</filename> files
 336               </para>
 337             </listitem>
 338           </varlistentry>
 339
 340         </variablelist> </para>
 341
 342     </sect2>
 343
 344     <sect2 id="database_setup">
 345       <title>(optional) &MYSQL; setup</title>
 346
 347       <para> To fully exploit &appname; indexing and search capabilities
 348         on a huge metadata set you may
 349         need a working &MYSQL; database. Detalied instructions on how to do
 350         it can be found in the <ulink type="http"
 351           url="http://dev.mysql.com/doc/">MySQL documentation</ulink>. Here you
 352         can find a quick howto. </para>
 353
 354       <para> In order to create a database you need administrator permissions on
 355         your MySQL installation, usually the root account has them. Once you
 356         have the permissions, a new database can be created executing
 357         <userinput>mysqladmin create matita</userinput>
 358         (<emphasis>matita</emphasis> is the default database name, you can
 359         change it using the <parameter>db.user</parameter> key of the
 360         configuration file). </para>
 361
 362       <para> Then you need to grant the necessary access permissions to the
 363         database user of &appname;, typing <userinput>echo "grant all privileges
 364           on matita.* to helm;" | mysql matita</userinput> should do the trick
 365         (<emphasis>helm</emphasis> is the default user name used by &appname; to
 366         access the database, you can change it using the
 367         <parameter>db.user</parameter> key of the configuration file).
 368       </para>
 369
 370       <note>
 371         <para> This way you create a database named <emphasis>matita</emphasis>
 372           on which anyone claiming to be the <emphasis>helm</emphasis> user can
 373           do everything (like adding dummy data or destroying the contained
 374           one). It is strongly suggested to apply more fine grained permissions,
 375           how to do it is out of the scope of this manual.</para>
 376       </note>
 377
 378     </sect2>
 379
 380     <sect2 id="build_instructions">
 381       <title>Compiling and installing</title>
 382
 383       <para> Once you get the source code the installations steps should be
 384         quite familiar.</para>
 385
 386       <para> First of all you need to configure the build process executing
 387         <userinput>./configure</userinput>. This will check that all needed
 388         tools and library are installed and prepare the sources for compilation
 389         and installation. </para>
 390
 391       <para> Quite a few (optional) arguments may be passed to the
 392         <application>configure</application> command line to change build time
 393         parameters. They are listed below, together with their
 394         default values: </para>
 395
 396         <variablelist>
 397           <title> <application>configure</application> command line
 398             arguments</title>
 399
 400           <varlistentry>
 401             <term>
 402               <userinput>--with-runtime-dir=<replaceable>dir</replaceable></userinput>
 403             </term>
 404             <listitem>
 405               <para>
 406                 (<emphasis>Default:</emphasis>
 407                 <filename>/usr/local/matita</filename>) Runtime base directory
 408                 where all &appname; stuff (executables, configuration files,
 409                 standard library, ...) will be installed
 410               </para>
 411             </listitem>
 412           </varlistentry>
 413
 414           <varlistentry>
 415             <term>
 416               <userinput>--with-dbhost=<replaceable>host</replaceable></userinput>
 417             </term>
 418             <listitem>
 419               <para>
 420                 (<emphasis>Default:</emphasis> localhost) Default SQL server
 421                 hostname. Will be used while building the standard library
 422                 during the installation and to create the default &appname;
 423                 configuration. May be changed later in configuration file.
 424               </para>
 425             </listitem>
 426           </varlistentry>
 427
 428           <varlistentry>
 429             <term>
 430               <userinput>--enable-debug</userinput>
 431             </term>
 432             <listitem>
 433               <para>
 434                 (<emphasis>Default:</emphasis> disabled) Enable debugging code.
 435                 Not for the casual user.
 436               </para>
 437             </listitem>
 438           </varlistentry>
 439         </variablelist>
 440
 441       <para> Then you will manage the build and install process using
 442         <application><ulink type="http"
 443             url="http://www.gnu.org/software/make/">make</ulink></application>
 444         as usual. Below are reported the targets you have to invoke in sequence
 445         to build and install:
 446       </para>
 447
 448         <variablelist>
 449           <title><application>make</application> targets</title>
 450
 451           <varlistentry>
 452             <term><userinput>world</userinput></term>
 453             <listitem>
 454               <para>builds components needed by &appname; and &appname; itself
 455                 (in bytecode or native code depending
 456                 on the availability of the OCaml native code compiler) </para>
 457             </listitem>
 458           </varlistentry>
 459
 460           <varlistentry>
 461             <term><userinput>install</userinput></term>
 462             <listitem>
 463               <para>installs &appname; related tools, standard library and the
 464                 needed runtime stuff in the proper places on the filesystem.
 465               </para>
 466               <para>As a part of the installation process the &appname;
 467                 standard library will be compiled, thus testing that the just
 468                 built <application>matitac</application> compiler works
 469                 properly.</para>
 470               <para>For this step you will need a working SQL database (for
 471                 indexing the standard library while you are compiling it). See
 472                 <ulink type="http" url="#database_setup">Database setup</ulink>
 473                 for instructions on how to set it up.
 474               </para>
 475             </listitem>
 476           </varlistentry>
 477
 478         </variablelist>
 479
 480     </sect2>
 481
 482   </sect1>
 483
 484   <sect1 id="matita.conf.xml">
 485     <title>Configuring &appname;</title>
 486     <para>
 487             The configuration file is divided in four sections. The user and
 488             matita ones are self explicative and does not need user
 489             intervention. Here we report a sample snippet for these two
 490             sections. The remaining db and getter sections will be explained in
 491             details later.
 492            <programlisting>
 493 <![CDATA[
 494   <section name="user">
 495     <key name="home">$(HOME)</key>
 496     <key name="name">$(USER)</key>
 497   </section>
 498   <section name="matita">
 499     <key name="basedir">$(user.home)/.matita</key>
 500     <key name="rt_base_dir">/usr/share/matita/</key>
 501     <key name="owner">$(user.name)</key>
 502   </section>
 503 ]]></programlisting>
 504     </para>
 505    <para>
 506            &appname; needs to store/fetch data and metadata. Data is essentially
 507            composed of XML files, metadata is a set of tuples for a relational
 508            model. Data and metadata can produced by the user or be already
 509            available. Both kind of data/metadata can be local and/or remote.
 510    </para>
 511    <para>
 512            The db section tells &appname; where to store and retrieve metadata,
 513            while the getter section describes where XML files have to be
 514            found. The following picture describes the suggested configuration.
 515            Dashed arrows are determined by the configuration file.
 516    </para>
 517    <figure><title>Configuring the Databases</title>
 518      <mediaobject>
 519        <imageobject>
 520          <imagedata fileref="figures/database.png" format="PNG" srccredit="Enrico Tassi"/>
 521        </imageobject>
 522        <textobject><phrase>How to configure the databases.</phrase></textobject>
 523      </mediaobject>
 524    </figure>
 525    <para>The getter</para>
 526    <para>
 527            Consider the following snippet and the URI
 528            <userinput>cic:/matita/foo/bar.con</userinput>. If &appname;
 529            is asked to read that object it will resolve the object trough
 530            the getter. Since the first two entries are equally specific
 531            (longest match rule applies) first the path
 532            <userinput>file://$(matita.rt_base_dir)/xml/standard-library/foo/bar.con</userinput>
 533            and then <userinput>file://$(user.home)/.matita/xml/matita/foo/bar.con</userinput>
 534            are inspected.
 535            <programlisting>
 536 <![CDATA[
 537   <section name="getter">
 538     <key name="cache_dir">$(user.home)/.matita/getter/cache</key>
 539     <key name="prefix">
 540       cic:/matita/
 541       file://$(matita.rt_base_dir)/xml/standard-library/
 542       ro
 543     </key>
 544     <key name="prefix">
 545       cic:/matita/
 546       file://$(user.home)/.matita/xml/matita/
 547     </key>
 548     <key name="prefix">
 549       cic:/Coq/
 550       http://mowgli.cs.unibo.it/xml/
 551       legacy
 552     </key>
 553   </section>
 554 ]]>
 555         </programlisting>
 556         if the same URI has to be written, the former prefix is skipped
 557         since it is marked as readonly (<userinput>ro</userinput>).
 558         Objects resolved using the third prefix are readonly too, and are
 559         retrieved using the network. There is no limit to the number of
 560         prefixes the user can define. The distinction between prefixes marked
 561         as readonly and legacy is that, legacy ones are really read only, while
 562         the ones marked with <userinput>ro</userinput> are considered for
 563         writing when &appname; is started in system mode (used to publish user
 564         developments in the library space).
 565    </para>
 566           <para>The db</para>
 567         <para>
 568            The database subsystem has three fron ends: library, user and
 569            legacy.  The latter is the only optional one. Every query is done on
 570            every frontend, making the duplicate free union of the results.
 571            The user front end kepps metadata produced by the user, and is thus
 572            heavily accessed in read/write mode, while the library and legacy
 573            fron ends are read only. Every front end can be connected to
 574            backend, the storage actually.
 575            Consider the following snippet.
 576            <programlisting>
 577 <![CDATA[
 578   <section name="db">
 579     <key name="metadata">mysql://mowgli.cs.unibo.it matita helm none legacy</key>
 580     <key name="metadata">file://$(matita.rt_base_dir) metadata.db helm helm library</key>
 581     <key name="metadata">file://$(matita.basedir) user.db helm helm user</key>
 582   </section>
 583 ]]>
 584         </programlisting>
 585         Here the usr database is a file (thus locally accessed trough the
 586         Sqlite library) placed in the user's home directory. The library one is
 587         placed in the &appname; runtime directory. The legacy fron end is
 588         connected to a remote &MYSQL; based storage. Every metadata key
 589         takes a path to the storage, the name of the database, the user name,
 590         a password (or <userinput>none</userinput>) and the name of the front
 591         end to which it is attached.
 592    </para>
 593   </sect1>
 594
 595 </chapter>
 596