matita/help/C/sec_install.xml

   1
   2 <!-- ============= Installation ============================== -->
   3
   4 <sect1 id="sec_install">
   5   <title>Installation</title>
   6
   7   <sect2>
   8     <title>Installing &appname; from sources</title>
   9
  10     <para>Currently, the only intended way to install &appname; is starting
  11       from its source code.  </para>
  12
  13     <sect3>
  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     </sect3>
  42
  43     <sect3 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&nbsp;<ulink type="http"
  58                 url="http://people.debian.org/~zack">http://people.debian.org/~zack</ulink>&nbsp;unstable&nbsp;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>
 175               <application> <ulink type="http"
 176                   url="http://www.mysql.com">MySQL</ulink> </application>
 177             </term>
 178             <term>
 179               <application> <ulink type="http"
 180                   url="http://raevnos.pennmush.org/code/ocaml-mysql/">OCaml
 181                   MySQL</ulink> </application>
 182             </term>
 183             <listitem>
 184               <para> SQL database and OCaml bindings for its client-side library
 185               </para>
 186               <para> The SQL database itself is not strictly needed to run
 187                 &appname;, but we stronly encourage its use since a lot of
 188                 features are disabled without it. Still, the OCaml bindings of
 189                 the library are needed at compile time.</para>
 190             </listitem>
 191           </varlistentry>
 192
 193           <varlistentry>
 194             <term>
 195               <application> <ulink type="http"
 196                   url="http://ocamlnet.sourceforge.net/">Ocamlnet</ulink>
 197               </application>
 198             </term>
 199             <listitem>
 200               <para> collection of OCaml libraries to deal with
 201                 application-level Internet protocols and conventions </para>
 202             </listitem>
 203           </varlistentry>
 204
 205           <varlistentry>
 206             <term>
 207               <application> <ulink type="http"
 208                   url="http://www.cduce.org/download.html#side">ulex</ulink>
 209               </application>
 210             </term>
 211             <listitem>
 212               <para> Unicode lexer generator for OCaml </para>
 213             </listitem>
 214           </varlistentry>
 215
 216           <varlistentry>
 217             <term>
 218               <application> <ulink type="http"
 219                   url="http://cristal.inria.fr/~xleroy/software.html#camlzip">CamlZip</ulink>
 220               </application>
 221             </term>
 222             <listitem>
 223               <para> OCaml library to access <filename>.gz</filename> files
 224               </para>
 225             </listitem>
 226           </varlistentry>
 227
 228         </variablelist> </para>
 229
 230     </sect3>
 231
 232     <sect3 id="build_instructions">
 233       <title>Instructions</title>
 234
 235       <para> Once you get the source code the installations steps should be
 236         quite familiar.</para>
 237
 238       <para> First of all you need to configure the build process executing
 239         <userinput>./configure</userinput>. This will check that all needed
 240         tools and library are installed. You may need to pass on the command
 241         line some of the parameters riported below:
 242
 243         <variablelist>
 244           <title><application>configure</application> parameters</title>
 245
 246           <varlistentry>
 247             <term>&TODO;</term>
 248             <listitem>&TODO;</listitem>
 249           </varlistentry>
 250
 251         </variablelist>
 252
 253       </para>
 254
 255       <para> Then you will manage the build process using <application><ulink
 256             type="http"
 257             url="http://www.gnu.org/software/make/">make</ulink></application>
 258         as usual. Below are reported the targets you have to invoke in sequence
 259         to build and install.
 260
 261         <variablelist>
 262           <title><application>make</application> targets</title>
 263
 264           <varlistentry>
 265             <term><userinput>world</userinput></term>
 266             <listitem>
 267               <para>builds components needed by &appname; and &appname; itself
 268                 (in bytecode only or in both bytecode and native code depending
 269                 on the availability of the OCaml native code compiler) </para>
 270             </listitem>
 271           </varlistentry>
 272
 273           <varlistentry>
 274             <term><userinput>library</userinput></term>
 275             <listitem>
 276               <para>uses the (just built) <application>matitac</application>
 277                 compiler to build the &appname; standard library. </para>
 278               <para>For this step you will need a working SQL database (for
 279                 indexing the standard library while you are compiling it). See
 280                 &TODO; for instructions on how to set it up.</para>
 281             </listitem>
 282           </varlistentry>
 283
 284           <varlistentry>
 285             <term><userinput>install</userinput></term>
 286             <listitem>
 287               <para>installs &appname; related tools, standard library and the
 288                 needed runtime stuff in the proper places on the filesystem
 289               </para>
 290             </listitem>
 291           </varlistentry>
 292
 293         </variablelist>
 294
 295       </para>
 296
 297     </sect3>
 298
 299   </sect2>
 300 </sect1>
 301