forked from coq/coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathINSTALL
299 lines (203 loc) · 10.7 KB
/
INSTALL
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
INSTALLATION PROCEDURES FOR THE COQ V8.6 SYSTEM
-----------------------------------------------
WHAT DO YOU NEED ?
==================
Your OS may already contain Coq under the form of a precompiled
package or ready-to-compile port. In this case, and if the supplied
version suits you, follow the usual procedure for your OS to
install it. E.g.:
- Debian GNU/Linux derivatives (or Debian GNU/k*BSD or ...):
aptitude install coq
- Gentoo GNU/Linux:
emerge sci-mathematics/coq
- Fedora GNU/Linux:
urpmi coq
- MacPorts for MacOS X
port install coq
To compile Coq V8.6 yourself, you need:
- OCaml version 4.02.1 or later
(available at http://caml.inria.fr/)
OCaml version 4.02.0 is not supported because of a severe performance
issue increasing compilation time.
- Findlib (included in OCaml binary distribution under windows,
probably available in your distribution and for sure at
http://projects.camlcity.org/projects/findlib.html)
- Camlp5 (version >= 6.02)
- GNU Make version 3.81 or later
- a C compiler
- for Coqide, the Lablgtk development files, and the GTK libraries
incuding gtksourceview, see INSTALL.ide for more details
QUICK INSTALLATION PROCEDURE.
=============================
1. ./configure
2. make
3. make install (you may need superuser rights)
INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
=================================================
1- Check that you have the Objective Caml compiler installed on your
computer and that "ocamlc" (or, better, its native code version
"ocamlc.opt") lies in a directory which is present in your $PATH
environment variable. At the time of writing this sentence, all
versions of Objective Caml later or equal to 4.02.1 are
supported.
To get Coq in native-code, (it runs 4 to 10 times faster than
bytecode, but it takes more time to get compiled and the binary is
bigger), you will also need the "ocamlopt" (or its native code version
"ocamlopt.opt") command.
2- Check that you have Camlp5 installed on your computer and that the
command "camlp5" lies in a directory which is present in your $PATH
environment variable path. (You need Camlp5 in both bytecode and
native versions if your platform supports it).
3- The uncompression and un-tarring of the distribution file gave birth
to a directory named "coq-8.xx". You can rename this directory and put
it wherever you want. Just keep in mind that you will need some spare
space during the compilation (reckon on about 300 Mb of disk space
for the whole system in native-code compilation). Once installed, the
binaries take about 30 Mb, and the library about 200 Mb.
4- First you need to configure the system. It is done automatically with
the command:
./configure <options>
The "configure" script will ask you for directories where to put
the Coq binaries, standard library, man pages, etc. It will propose
you some default values.
For a list of options accepted by the "configure" script, run
"./configure -help". The main options accepted are:
-prefix <dir>
Binaries, library, man pages and Emacs mode will be respectively
installed in <dir>/bin, <dir>/lib/coq, <dir>/man and
<dir>/lib/emacs/site-lisp
-bindir <dir> (default: /usr/local/bin)
Directory where the binaries will be installed
-libdir <dir> (default: /usr/local/lib/coq)
Directory where the Coq standard library will be installed
-mandir <dir> (default: /usr/local/share/man)
Directory where the Coq manual pages will be installed
-emacslib <dir> (default: /usr/local/lib/emacs/site-lisp)
Directory where the Coq Emacs mode will be installed
-arch <value> (default is the result of the command "arch")
An arbitrary architecture name for your machine (useful when
compiling Coq on two different architectures for which the
result of "arch" is the same, e.g. Sun OS and Solaris)
-local
Compile Coq to run in its source directory. The installation (step 6)
is not necessary in that case.
-browser <command>
Use <command> to open an URL in a browser. %s must appear in <command>,
and will be replaced by the URL.
5- Still in the root directory, do
make
to compile Coq in the best OCaml mode available (native-code if supported,
bytecode otherwise).
This will compile the entire system. This phase can take more or less time,
depending on your architecture and is fairly verbose. On a multi-core machine,
it is recommended to compile in parallel, via make -jN where N is your number
of cores.
6- You can now install the Coq system. Executables, libraries, manual pages
and emacs mode are copied in some standard places of your system, defined at
configuration time (step 3). Just do
umask 022
make install
Of course, you may need superuser rights to do that.
To use the Coq emacs mode you also need to put the following lines
in you .emacs file:
(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
(autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
7- Optionally, you could build the bytecode version of Coq via:
make byte
and install it via
make install-byte
This version is quite slower than the native code version of Coq, but could
be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml
toplevel accessible via the Drop command.
8- You can now clean all the sources. (You can even erase them.)
make clean
INSTALLATION PROCEDURE FOR ADVANCED USERS.
==========================================
If you wish to write plugins you *must* keep the Coq sources, without
cleaning them. Therefore, to avoid a duplication of binaries and library,
it is not necessary to do the installation step (6- above). You just have
to tell it at configuration step (4- above) with the option -local :
./configure -local <other options>
Then compile the sources as described in step 5 above. The resulting
binaries will reside in the subdirectory bin/.
Unless you pass the -nodebug option to ./configure, the -g option of the
OCaml compiler will be used during compilation to allow debugging.
See the debugging file in dev/doc and the chapter 15 of the Coq Reference
Manual for details about how to use the OCaml debugger with Coq.
THE AVAILABLE COMMANDS.
=======================
There are two Coq commands:
coqtop The Coq toplevel
coqc The Coq compiler
Under architecture where ocamlopt is available, coqtop is the native code
version of Coq. On such architecture, you could additionally request
the build of the bytecode version of Coq via 'make byte' and install it via
'make install-byte'. This will create an extra binary named coqtop.byte,
that could be used for debugging purpose. If native code isn't available,
coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte.
coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop
and coqc selects a particular binary.
* `coqtop' launches Coq in the interactive mode. By default it loads
basic logical definitions and tactics from the Init directory.
* `coqc' allows compilation of Coq files directly from the command line.
To compile a file foo.v, do:
coqc foo.v
It will produce a file foo.vo, that you can now load through the Coq
command "Require".
A detailed description of these commands and of their options is given
in the Reference Manual (which you can get in the doc/
directory, or read online on http://coq.inria.fr/doc/)
and in the corresponding manual pages.
There is also a tutorial and a FAQ; see http://coq.inria.fr/getting-started
COMPILING FOR DIFFERENT ARCHITECTURES.
======================================
This section explains how to compile Coq for several architecture, sharing
the same sources. The important fact is that some files are architecture
dependent (.cmx, .o and executable files for instance) but others are not
(.cmo and .vo). Consequently, you can :
o save some time during compilation by not cleaning the architecture
independent files;
o save some space during installation by sharing the Coq standard
library (which is fully architecture independent).
So, in order to compile Coq for a new architecture, proceed as follows:
* Omit step 7 above and clean only the architecture dependent files:
it is done automatically with the command
make archclean
* Configure the system for the new architecture:
./configure <options>
You can specify the same directory for the standard library but you
MUST specify a different directory for the binaries (of course).
* Compile and install the system as described in steps 5 and 6 above.
MOVING BINARIES OR LIBRARY.
===========================
If you move both the binaries and the library in a consistent way,
Coq should be able to still run. Otherwise, Coq may be "lost",
running "coqtop" would then return an error message of the kind:
Error during initialization :
Error: cannot guess a path for Coq libraries; please use -coqlib option
You can then indicate the new places to Coq, using the options -coqlib :
coqtop -coqlib <new directory>
See also next section.
DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
======================================================
Some bytecode executables of Coq use the OCaml runtime, which dynamically
loads a shared library (.so or .dll). When it is not installed properly, you
can get an error message of this kind:
Fatal error: cannot load shared library dllcoqrun
Reason: dllcoqrun.so: cannot open shared object file: No such file or directory
In this case, you need either:
- to set the CAML_LD_LIBRARY_PATH environment variable to point to the
directory where dllcoqrun.so is; this is suitable when you want to run
the command a limited number of times in a controlled environment (e.g.
during compilation of binary packages);
- install dllcoqrun.so in a location listed in the file ld.conf that is in
the directory of the standard library of OCaml;
- recompile your bytecode executables after reconfiguring the location
of the shared library:
./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ...
where <path> is the directory where the dllcoqrun.so is installed;
- (not recommended) compile bytecode executables with a custom OCaml
runtime by using:
./configure -custom ...
be aware that stripping executables generated this way, or performing
other executable-specific operations, will make them useless.