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