[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


Author: notin
Date: 2009-02-17 16:58:54 +0100 (Tue, 17 Feb 2009)
New Revision: 11934

Modified:
   tags/V8.2-1/INSTALL
   tags/V8.2-1/INSTALL.macosx
   tags/V8.2-1/README
   tags/V8.2-1/README.win
   tags/V8.2-1/configure
Log:
Pr?\195?\169paration de la release

Modified: tags/V8.2-1/INSTALL
===================================================================
--- 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
+   document.
 
 
 QUICK INSTALLATION PROCEDURE.
@@ -99,21 +101,18 @@
    bigger), you will also need the "ocamlopt" (or its native code version
    "ocamlopt.opt") command.
 
-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
    the command:
@@ -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.
 ======================================================
 

Modified: tags/V8.2-1/INSTALL.macosx
===================================================================
--- 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
+http://logical.saclay.inria.fr/coq-bugs).

Modified: tags/V8.2-1/README
===================================================================
--- 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 @@
 DOCUMENTATION.
 ==============
 
-   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
-   http://coq.inria.fr/doc-eng.html.
+   The documentation of Coq V8.2 is available online from the Coq web
+   site (see http://coq.inria.fr)
 
 
 CHANGES.
@@ -27,10 +26,10 @@
 AVAILABILITY.
 =============
 
-   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 (192.93.2.54)
-	directory:  INRIA/LogiCal/coq/
 
 THE COQ CLUB.
 =============
@@ -68,12 +67,8 @@
 
    Send your bug reports by filling a form at
 
-        http://coq.inria.fr/bin/coq-bugs
+        http://logical.saclay.inria.fr/coq-bugs
 
-   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.

Modified: tags/V8.2-1/README.win
===================================================================
--- 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.
 
 INSTALLATION.
 =============
@@ -16,12 +16,19 @@
 COMPILATION.
 ============
 
-    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.
        See: http://caml.inria.fr
+     
+       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:
        http://www.cygwin.com
 
-    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
        See: http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
 
        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
 
         ./configure
         make world
         make install
 
-    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.

Modified: tags/V8.2-1/configure
===================================================================
--- 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 @@
 # 
 ##################################
 
-VERSION=8.2-1
-VOMAGIC=08201 
-STATEMAGIC=19765
+VERSION=8.2
+VOMAGIC=08200 
+STATEMAGIC=58200
 DATE=`LANG=C date +"%B %Y"`
 
 # Create the bin/ directory if non-existent





Plus d'informations sur la liste de diffusion Coq-commits