2 Tiny Matita logoMatita Home
4 Chapter 2. Installation
7 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
9 Chapter 2. Installation
13 Installing from sources
15 Getting the source code
18 Compiling and installing
22 Installing from sources
24 Currently, the only intended way to install Matita is starting from its source
27 Getting the source code
29 You can get the Matita source code in two ways:
31 1. go to the download page and get the latest released source tarball;
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.
37 In this case you will need to run autoconf before proceding with the
38 building instructions below.
42 In order to build Matita from sources you will need some tools and libraries.
43 They are listed below.
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 /
51 deb http://people.debian.org/~zack unstable helm
54 and installing the helm-matita-deps package.
56 Required tools and libraries
60 the Objective Caml compiler, version 3.09 or above
64 OCaml package manager, version 1.1.1 or above
68 OCaml bindings for the expat library
72 OCaml bindings for the Gdome 2 library
76 OCaml library to write HTTP daemons (and clients)
80 OCaml bindings for the GTK+ library , version 2.6.0 or above
82 GtkMathView , LablGtkMathView
84 GTK+ widget to render MathML documents and its OCaml bindings
86 GtkSourceView , LablGtkSourceView
88 extension for the GTK+ text widget (adding the typical features of source
89 code editors) and its OCaml bindings
93 SQL database and OCaml bindings for its client-side library
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.
101 collection of OCaml libraries to deal with application-level Internet
102 protocols and conventions
106 Unicode lexer generator for OCaml
110 OCaml library to access .gz files
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.
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
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).
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.
136 Compiling and installing
138 Once you get the source code the installations steps should be quite familiar.
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.
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
148 configure command line arguments
150 --with-runtime-dir=dir
152 (Default: /usr/local/matita) Runtime base directory where all Matita stuff
153 (executables, configuration files, standard library, ...) will be installed
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.
163 (Default: disabled) Enable debugging code. Not for the casual user.
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:
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)
177 installs Matita related tools, standard library and the needed runtime
178 stuff in the proper places on the filesystem.
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.
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.
187 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
190 Matita vs Coq Home Configuring Matita