helm/software/matita/dist/INSTALL

   1 Chapter 2. Installation
   2
   3 Table of Contents
   4
   5 Installing from sources
   6
   7     Getting the source code
   8     Requirements
   9     Database setup
  10     Compiling and installing
  11
  12 Installing from sources
  13
  14 Currently, the only intended way to install Matita is starting from its source
  15 code.
  16
  17 Getting the source code
  18
  19 You can get the Matita source code in two ways:
  20
  21  1. go to the download page and get the latest released source tarball;
  22
  23  2. get the development sources from our SVN repository. You will need the
  24     components/ and matita/ directories from the trunk/helm/software/
  25     directory, plus the configure and Makefile* stuff from the same directory.
  26
  27     In this case you will need to run autoconf before proceding with the
  28     building instructions below.
  29
  30 Requirements
  31
  32 In order to build Matita from sources you will need some tools and libraries.
  33 They are listed below.
  34
  35 Note for Debian users
  36
  37 If you are running a Debian GNU/Linux distribution you can have APT install all
  38 the required tools and libraries by adding the following repository to your /
  39 etc/apt/sources.list:
  40
  41               deb http://people.debian.org/~zack unstable helm
  42
  43
  44 and installing the helm-matita-deps package.
  45
  46 Required tools and libraries
  47
  48 OCaml
  49
  50     the Objective Caml compiler, version 3.09 or above
  51
  52 Findlib
  53
  54     OCaml package manager, version 1.1.1 or above
  55
  56 OCaml Expat
  57
  58     OCaml bindings for the expat library
  59
  60 GMetaDOM
  61
  62     OCaml bindings for the Gdome 2 library
  63
  64 OCaml HTTP
  65
  66     OCaml library to write HTTP daemons (and clients)
  67
  68 LablGTK
  69
  70     OCaml bindings for the GTK+ library , version 2.6.0 or above
  71
  72 GtkMathView , LablGtkMathView
  73
  74     GTK+ widget to render MathML documents and its OCaml bindings
  75
  76 GtkSourceView , LablGtkSourceView
  77
  78     extension for the GTK+ text widget (adding the typical features of source
  79     code editors) and its OCaml bindings
  80
  81 MySQL , OCaml MySQL
  82
  83     SQL database and OCaml bindings for its client-side library
  84
  85     The SQL database itself is not strictly needed to run Matita, but we
  86     stronly encourage its use since a lot of features are disabled without it.
  87     Still, the OCaml bindings of the library are needed at compile time.
  88
  89 Ocamlnet
  90
  91     collection of OCaml libraries to deal with application-level Internet
  92     protocols and conventions
  93
  94 ulex
  95
  96     Unicode lexer generator for OCaml
  97
  98 CamlZip
  99
 100     OCaml library to access .gz files
 101
 102 Database setup
 103
 104 To fully exploit Matita indexing and search capabilities you will need a
 105 working MySQL database. Detalied instructions on how to do it can be found in
 106 the MySQL documentation. Here you can find a quick howto.
 107
 108 In order to create a database you need administrator permissions on your MySQL
 109 installation, usually the root account has them. Once you have the permissions,
 110 a new database can be created executing mysqladmin create matita (matita is the
 111 default database name, you can change it using the db.user key of the
 112 configuration file).
 113
 114 Then you need to grant the necessary access permissions to the database user of
 115 Matita, typing echo "grant all privileges on matita.* to helm;" | mysql matita
 116 should do the trick (helm is the default user name used by Matita to access the
 117 database, you can change it using the db.user key of the configuration file).
 118
 119 Note
 120
 121 This way you create a database named matita on which anyone claiming to be the
 122 helm user can do everything (like adding dummy data or destroying the contained
 123 one). It is strongly suggested to apply more fine grained permissions, how to
 124 do it is out of the scope of this manual.
 125
 126 Compiling and installing
 127
 128 Once you get the source code the installations steps should be quite familiar.
 129
 130 First of all you need to configure the build process executing ./configure.
 131 This will check that all needed tools and library are installed and prepare the
 132 sources for compilation and installation.
 133
 134 Quite a few (optional) arguments may be passed to the configure command line to
 135 change build time parameters. They are listed in the table below, together with
 136 their default values.
 137
 138 Table 2.1.  configure command line arguments
 139
 140 ┌──────────────────┬─────────┬────────────────────────────────────────────────┐
 141 │     Argument     │ Default │                  Description                   │
 142 ├──────────────────┼─────────┼────────────────────────────────────────────────┤
 143 │--with-runtime-dir│/usr/    │Runtime base directory where all Matita stuff   │
 144 │=dir              │local/   │(executables, configuration files, standard     │
 145 │                  │matita/  │library, ...) will be installed                 │
 146 ├──────────────────┼─────────┼────────────────────────────────────────────────┤
 147 │                  │         │Default SQL server hostname. Will be used while │
 148 │                  │         │building the standard library during the        │
 149 │--with-dbhost=host│localhost│installation and to create the default Matita   │
 150 │                  │         │configuration. May be changed later in          │
 151 │                  │         │configuration file.                             │
 152 ├──────────────────┼─────────┼────────────────────────────────────────────────┤
 153 │--enable-debug    │disabled │Enable debugging code. Not for the casual user. │
 154 └──────────────────┴─────────┴────────────────────────────────────────────────┘
 155
 156 Then you will manage the build and install process using make as usual. Below
 157 are reported the targets you have to invoke in sequence to build and install.
 158
 159 make targets
 160
 161 world
 162
 163     builds components needed by Matita and Matita itself (in bytecode only or
 164     in both bytecode and native code depending on the availability of the OCaml
 165     native code compiler)
 166
 167 library
 168
 169     uses the (just built) matitac compiler to build the Matita standard
 170     library.
 171
 172     For this step you will need a working SQL database (for indexing the
 173     standard library while you are compiling it). See Database setup for
 174     instructions on how to set it up.
 175
 176 install
 177
 178     installs Matita related tools, standard library and the needed runtime
 179     stuff in the proper places on the filesystem
 180