]> matita.cs.unibo.it Git - helm.git/blob - matita/dist/INSTALL
closed all axioms
[helm.git] / 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