helm/software/matita/dist/INSTALL

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