helm/www/matita/install.html

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