4
The Coq documentation includes
8
- A document presenting the Coq standard library
9
- A list of questions/answers in the FAQ style
11
The sources of the documents are mainly made of LaTeX code from which
12
user-readable PostScript or PDF files, or a user-browsable bunch of
13
html files are generated.
18
To produce the documents, you need the coqtop, coq-tex, coqdoc and
19
gallina tools, with same version number as the current
20
documentation. These four tools normally come with any basic Coq
23
In addition, to produce the PostScript documents, the following tools
30
- pngtopnm and pnmtops (for the Reference Manual and the FAQ)
32
To produce the PDF documents, the following tools are needed:
37
To produce the html documents, the following tools are needed:
39
- hevea (e.g. 1.07 works)
41
To produce the documentation of the standard library, a source copy of
42
the coq distribution is needed.
47
To produce all PostScript documents, do: make all-ps
48
To produce all PDF documents, do: make all-pdf
49
To produce all html documents, do: make all-html
50
To produce all formats of the Reference Manual, do: make refman
51
To produce all formats of the Tutorial, do: make tutorial
52
To produce all formats of the Coq Standard Library, do: make stdlib
53
To produce all formats of the FAQ, do: make faq
58
To install all produced documents, do:
60
make DOCDIR=/some/directory/for/documentation install
62
DOCDIR defauts to /usr/share/doc/coq-x.y were x.y is the version number
2
INSTALLATION PROCEDURES FOR THE COQ V8.2 SYSTEM
3
-----------------------------------------------
9
Coq is designed to work on computers equipped with a POSIX (Unix or
10
a clone) operating system. It also works under Microsoft Windows
11
(see INSTALL.win); for a precompiled MacOS X package, see
14
Coq is known to be actively used under GNU/Linux (i386, amd64 and
15
ppc) and FreeBSD. Automated tests are run under many, many
16
different architectures under GNU/Linux.
18
Naturally, Coq will run faster on an architecture where OCaml can
19
compile to native code, rather than only bytecode. At time of
20
writing, that is IA32, PowerPC, AMD64, Alpha, Sparc, Mips, IA64,
21
HPPA and StrongArm. See
22
http://caml.inria.fr/ocaml/portability.en.html for details.
25
Your OS may already contain Coq under the form of a precompiled
26
package or ready-to-compile port. In this case, and if the supplied
27
version suits you, follow the usual procedure for your OS to
30
- Debian GNU/Linux (or Debian GNU/k*BSD or ...):
36
emerge sci-mathematics/coq
42
Should you need or prefer to compile Coq V8.2 yourself, you need:
44
- Objective Caml version 3.07 or later
45
(available at http://caml.inria.fr/)
47
For Ocaml version >= 3.10.0, you also need to install camlp5
48
(version <= 4.08, or >= 5.01 transitional)
51
- GNU Make version 3.81 or later
53
available at http://www.gnu.org/software/make/, but also a
54
standard or optional add-on part to most Unices and Unix
55
clones, sometimes under the name "gmake".
57
If a new enough version is not included in your system, nor
58
easily available as an add-on, this should get you a working
61
#Download it (wget is an example, use your favourite FTP or HTTP client)
62
wget http://ftp.gnu.org/pub/gnu/make/make-3.81.tar.bz2
63
bzip2 -cd make-3.81.tar.bz2 | tar x
64
#If you don't have bzip2, you can download the gzipped version instead.
66
./configure --prefix=${HOME}
69
Then, make sure that ${HOME}/bin is first in your $PATH.
74
- for Coqide, the Lablgtk development files, and the GTK
75
libraries, see INSTALL.ide for more details
77
Coq sources distribution comes as a single compressed tar-file. You
78
have probably already decompressed it if you are reading this
82
QUICK INSTALLATION PROCEDURE.
83
=============================
87
3. make install (you may need superuser rights)
91
INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
92
=================================================
94
1- Check that you have the Objective Caml compiler version 3.07 (or later)
95
installed on your computer and that "ocamlmktop" and "ocamlc" (or
96
its native code version "ocamlc.opt") lie in a directory which is present
97
in your $PATH environment variable.
99
To get Coq in native-code, (it runs 4 to 10 times faster than
100
bytecode, but it takes more time to get compiled and the binary is
101
bigger), you will also need the "ocamlopt" (or its native code version
102
"ocamlopt.opt") command.
104
2- If you are using OCaml version >= 3.10.0, check that you have
105
Camlp5 installed on your computer and that the command "camlp5"
106
lies in a directory which is present in your $PATH environment
107
variable path. (You need Camlp5 in both bytecode and native
108
versions if your platform supports it).
110
3- The uncompression and un-tarring of the distribution file gave birth
111
to a directory named "coq-8.xx". You can rename this directory and put
112
it wherever you want. Just keep in mind that you will need some spare
113
space during the compilation (reckon on about 250 Mb of disk space
114
for the whole system in native-code compilation). Once installed, the
115
binaries take about 65 Mb, and the library about 60 Mb.
117
4- First you need to configure the system. It is done automatically with
120
./configure <options>
122
The "configure" script will ask you for directories where to put
123
the Coq binaries, standard library, man pages, etc. It will propose
124
you some default values.
126
For a list of options accepted by the "configure" script, run
127
"./configure -help". The main options accepted are:
130
Binaries, library, man pages and Emacs mode will be respectively
131
installed in <dir>/bin, <dir>/lib/coq, <dir>/man and
132
<dir>/lib/emacs/site-lisp
134
-bindir <dir> (default: /usr/local/bin)
135
Directory where the binaries will be installed
137
-libdir <dir> (default: /usr/local/lib/coq)
138
Directory where the Coq standard library will be installed
140
-mandir <dir> (default: /usr/local/man)
141
Directory where the Coq manual pages will be installed
143
-emacslib <dir> (default: /usr/local/lib/emacs/site-lisp)
144
Directory where the Coq Emacs mode will be installed
146
-arch <value> (default is the result of the command "arch")
147
An arbitrary architecture name for your machine (useful when
148
compiling Coq on two different architectures for which the
149
result of "arch" is the same, e.g. Sun OS and Solaris)
152
Compile Coq to run in its source directory. The installation (step 6)
153
is not necessary in that case.
156
Use the ocamlc.opt compiler instead of ocamlc (and ocamlopt.opt
157
compiler instead of ocamlopt). Makes compilation faster (recommended).
160
Disable the Objective Caml compiler warnings. This option has no
161
effect on the result of the compilation.
164
Use <command> to open an URL in a browser. %s must appear in <command>,
165
and will be replaced by the URL.
167
5- Still in the root directory, do
171
to compile Coq in Objective Caml bytecode (and native-code if supported).
173
This will compile the entire system. This phase can take more or less time,
174
depending on your architecture and is fairly verbose.
176
6- You can now install the Coq system. Executables, libraries, manual pages
177
and emacs mode are copied in some standard places of your system, defined at
178
configuration time (step 3). Just do
183
Of course, you may need superuser rights to do that.
184
To use the Coq emacs mode you also need to put the following lines
187
(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
188
(autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
190
7- You can now clean all the sources. (You can even erase them.)
195
INSTALLATION PROCEDURE FOR ADVANCED USERS.
196
==========================================
198
If you wish to write tactics (and that really means that you belong
199
to advanced users!) you *must* keep the Coq sources, without cleaning
200
them. Therefore, to avoid a duplication of binaries and library, it is
201
not necessary to do the installation step (6- above).
202
You just have to tell it at configuration step (4- above) with the
205
./configure -local <other options>
207
Then compile the sources as described in step 5 above. The resulting
208
binaries will reside in the subdirectory bin/.
210
If you want to compile the sources for debugging (i.e. with the option
211
-g of the Caml compiler) then add the -debug option at configuration
214
./configure -debug <other options>
216
and then compile the sources (step 5). Then you must make a Coq toplevel
217
including your own tactics, which must be compiled with -g, with coqmktop.
218
See the chapter 16 of the Coq Reference Manual for details about how
219
to use coqmktop and the Objective Caml debugger with Coq.
222
THE AVAILABLE COMMANDS.
223
=======================
225
There are two Coq commands:
227
coqtop The Coq toplevel
228
coqc The Coq compiler
230
There are actually two binaries for the interactive system, coqtop.byte
231
and coqtop.opt (respectively bytecode and native code versions of Coq).
232
coqtop is a link to the fastest version, i.e. coqtop.opt if any, and
233
coqtop.byte otherwise. coqc also invokes the fastest version of Coq.
234
Options -opt and -byte to coqtop and coqc selects a particular binary.
236
* `coqtop' launches Coq in the interactive mode. The default state
237
(see the "-inputstate" option) is `initial.coq', which contains some
238
basic logical definitions, the associated parsing and printing rules,
239
and the following tactic modules: Equality, Tauto, Inv, EAuto and Refine.
241
* `coqc' allows compilation of Coq files directly from the command line.
242
To compile a file foo.v, do:
246
It will produce a file foo.vo, that you can now load through the Coq
249
A detailed description of these commands and of their options is given
250
in the Reference Manual (which you can get by FTP, in the doc/
251
directory, or read online on http://coq.inria.fr/doc/)
252
and in the corresponding manual pages.
254
There is also a tutorial and a FAQ; see http://coq.inria.fr/doc1-eng.html
260
* On some sites, when running `./configure', `pwd' returned a
261
path which is not valid from another machine (it may look like
262
"/tmp_mnt/foo/...") and, as a consequence, you won't be able to run
263
coqtop or coqc. The solution is to give the correct value, with
265
./configure -src <correct path> <other options>
267
* The `make install' procedure uses mkdirhier, a program that may
268
not be present on certain systems. To fix that, try to replace
269
mkdirhier with mkdir -p
271
* See also section on dynamically loaded libraries.
274
COMPILING FOR DIFFERENT ARCHITECTURES.
275
======================================
277
This section explains how to compile Coq for several architecture,
278
sharing the same sources. The important fact is that some files are
279
architecture dependent (.cmx, .o and executable files for instance)
280
but others are not (.cmo and .vo). Consequently, you can :
282
o save some time during compilation by not cleaning the architecture
285
o save some space during installation by sharing the Coq standard
286
library (which is fully architecture independent).
288
So, in order to compile Coq for a new architecture, proceed as follows:
290
* Omit step 7 above and clean only the architecture dependent files:
291
it is done automatically with the command
295
* Configure the system for the new architecture:
297
./configure <options>
299
You can specify the same directory for the standard library but you
300
MUST specify a different directory for the binaries (of course).
302
* Compile and install the system as described in steps 5 and 6 above.
305
MOVING BINARIES OR LIBRARY.
306
===========================
308
If you move the binaries or the library, Coq will be "lost".
309
Running "coqtop" would then return an error message of the kind:
311
Error during initialization :
312
Error: Can't find file initial.coq on loadpath
314
If you really have (or want) to move the binaries or the library, then
315
you have to indicate where Coq will find the libraries:
317
coqtop -coqlib <directory>
320
DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
321
======================================================
323
Some bytecode executables of Coq use the OCaml runtime, which dynamically
324
loads a shared library (.so or .dll). When it is not installed properly, you
325
can get an error message of this kind:
327
Fatal error: cannot load shared library dllcoqrun
328
Reason: dllcoqrun.so: cannot open shared object file: No such file or directory
330
In this case, you need either:
331
- to set the CAML_LD_LIBRARY_PATH environment variable to point to the
332
directory where dllcoqrun.so is; this is suitable when you want to run
333
the command a limited number of times in a controlled environment (e.g.
334
during compilation of binary packages);
335
- install dllcoqrun.so in a location listed in the file ld.conf that is in
336
the directory of the standard library of OCaml;
337
- recompile your bytecode executables after reconfiguring the location of
338
of the shared library:
339
./configure -coqrunbyteflags "-dllib -lcoqrun -dllpath <path>" ...
340
where <path> is the directory where the dllcoqrun.so is installed;
341
- (not recommended) compile bytecode executables with a custom OCaml
343
./configure -custom ...
344
be aware that stripping executables generated this way, or performing
345
other executable-specific operations, will make them useless.
added
removed
INSTALL
