[Coq-commits] r11934 - tags/V8.2-1
notin at users.gforge.inria.fr
notin at users.gforge.inria.fr
Mar 17 Fév 16:58:59 CET 2009
Date: 2009-02-17 16:58:54 +0100 (Tue, 17 Feb 2009)
New Revision: 11934
Pr?\195?\169paration de la release
--- tags/V8.2-1/INSTALL 2009-02-17 14:12:05 UTC (rev 11933)
+++ tags/V8.2-1/INSTALL 2009-02-17 15:58:54 UTC (rev 11934)
@@ -71,10 +71,12 @@
- a C compiler
- - for Coqide, the Lablgtk development files, and the GTK libraries, see INSTALL.ide for more details
+ - for Coqide, the Lablgtk development files, and the GTK
+ libraries, see INSTALL.ide for more details
- By FTP, Coq comes as a single compressed tar-file. You have
- probably already decompressed it if you are reading this document.
+ Coq sources distribution comes as a single compressed tar-file. You
+ have probably already decompressed it if you are reading this
QUICK INSTALLATION PROCEDURE.
@@ -99,21 +101,18 @@
bigger), you will also need the "ocamlopt" (or its native code version
-2- Check that you have Camlp4 installed on your
- computer and that the command "camlp4" lies in a directory which
- is present in your $PATH environment variable path.
- (You need Camlp4 in both bytecode and native versions if
- your platform supports it).
+2- If you are using OCaml version >= 3.10.0, 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).
- Note: in the latest ocaml distributions, camlp4 comes with ocaml so
- you do not have to check this point anymore.
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 50 Mb of disk space
+ space during the compilation (reckon on about 250 Mb of disk space
for the whole system in native-code compilation). Once installed, the
- binaries take about 14 Mb, and the library about 9 Mb.
+ binaries take about 65 Mb, and the library about 60 Mb.
4- First you need to configure the system. It is done automatically with
@@ -313,14 +312,11 @@
Error: Can't find file initial.coq on loadpath
If you really have (or want) to move the binaries or the library, then
- you have to indicate their new places to Coq, using the options -bindir (for
- the binaries directory) and -libdir (for the standard library directory) :
+ you have to indicate where Coq will find the libraries:
- coqtop -bindir <new directory> -libdir <new directory>
+ coqtop -coqlib <directory>
- See also next section.
DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
--- tags/V8.2-1/INSTALL.macosx 2009-02-17 14:12:05 UTC (rev 11933)
+++ tags/V8.2-1/INSTALL.macosx 2009-02-17 15:58:54 UTC (rev 11934)
@@ -16,5 +16,6 @@
can be used from a Terminal window: the interactive toplevel is
named coqtop and the compiler is coqc.
-If you have any trouble with this installation, please contact:
-coq-bugs at pauillac.inria.fr.
+If you have any trouble with this installation, please consider using
+our bug tracking system to report bug (see
--- tags/V8.2-1/README 2009-02-17 14:12:05 UTC (rev 11933)
+++ tags/V8.2-1/README 2009-02-17 15:58:54 UTC (rev 11934)
@@ -11,9 +11,8 @@
- The documentation of Coq V8.2 is available by anonymous ftp (see below),
- in a directory doc/. It is also available on Coq web site at
+ The documentation of Coq V8.2 is available online from the Coq web
+ site (see http://coq.inria.fr)
@@ -27,10 +26,10 @@
- Coq is available by anonymous FTP on ftp.inria.fr:
+ Coq is available as a precompiled package from the major linux
+ distributions. It is also available for Windows and Mac OS systems
+ from the Coq web site (see http://coq.inria.fr).
- host: ftp.inria.fr (22.214.171.124)
- directory: INRIA/LogiCal/coq/
THE COQ CLUB.
@@ -68,12 +67,8 @@
Send your bug reports by filling a form at
- or by E-mail to
- coq-bugs at coq.inria.fr
To be effective, bug reports should mention the Caml version used
to compile and run Coq, the Coq version (coqtop -v), the configuration
used, and include a complete source example leading to the bug.
--- tags/V8.2-1/README.win 2009-02-17 14:12:05 UTC (rev 11933)
+++ tags/V8.2-1/README.win 2009-02-17 15:58:54 UTC (rev 11934)
@@ -1,7 +1,7 @@
THE COQ V8.2 SYSTEM
- This file contains remarks specific to the windows port of Coq.
+ This file contains remarks specific to the Windows port of Coq.
@@ -16,12 +16,19 @@
- If you want to install coq, you had better transfer the precompiled
+ If you want to install Coq, you had better transfer the precompiled
distribution. If you really need to recompile under Windows, here
are some indications:
- 1- Install ocaml for Windows (MinGW port), preferably version 3.09.3.
+ 1- Install OCaml for Windows (MinGW port), preferably version 3.11.0.
+ If you choose OCaml 3.11.0, you also need to install FlexDLL.
+ See: http://alain.frisch.fr/flexdll.html
+ As shell script really dislikes space character within file
+ names, we strongly advise you to install OCaml to a path not
+ containing spaces, like 'C:\OCaml'
2- Install a shell environment with at least:
- a C compiler (gcc),
@@ -31,19 +38,22 @@
(official packages are made using Cygwin) See:
- 3- In order to compile Coqide, you will need the LablGTK library
+ 3- If using OCaml version >= 3.10.0, you have to install Camlp5.
+ See http://pauillac.inria.fr/~ddr/camlp5/
+ 4- In order to compile Coqide, you will need the LablGTK library
You also need to install the GTK libraries for Windows (see the
installation instruction for LablGTK)
- 4- In a shell window, type successively
+ 5- In a shell window, type successively
- 5- Though not nescessary, you can find useful:
+ 6- Though not nescessary, you can find useful:
- Windows version of (X)Emacs: it is a powerful environment for
developpers with coloured syntax, modes for compilation and debug,
and many more. It is free. See: http://www.gnu.org/software.
--- tags/V8.2-1/configure 2009-02-17 14:12:05 UTC (rev 11933)
+++ tags/V8.2-1/configure 2009-02-17 15:58:54 UTC (rev 11934)
@@ -6,9 +6,9 @@
DATE=`LANG=C date +"%B %Y"`
# Create the bin/ directory if non-existent
Plus d'informations sur la liste de diffusion Coq-commits