From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- INSTALL | 167 ++++++++++++++++++++++++---------------------------------------- 1 file changed, 63 insertions(+), 104 deletions(-) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index 15f1b90a..2b387b01 100644 --- a/INSTALL +++ b/INSTALL @@ -1,24 +1,21 @@ - INSTALLATION PROCEDURES FOR THE COQ V8.4 SYSTEM + INSTALLATION PROCEDURES FOR THE COQ V8.5 SYSTEM ----------------------------------------------- WHAT DO YOU NEED ? ================== - Coq is designed to work on computers equipped with a POSIX (Unix or - a clone) operating system. It also works under Microsoft Windows - (see INSTALL.win); for a precompiled MacOS X package, see - INSTALL.macosx. + Coq is designed to work on computers equipped with a POSIX (Unix or a + clone) operating system. It also works under Microsoft Windows (see + INSTALL.win); for a MacOS X bundle application, see INSTALL.macosx. - Coq is known to be actively used under GNU/Linux (i386, amd64 and - ppc) and FreeBSD. Automated tests are run under many, many - different architectures under GNU/Linux. + Coq is known to be actively used under GNU/Linux (i386 and amd64) and + FreeBSD. Automated tests are run under many, many different architectures + under GNU/Linux. - Naturally, Coq will run faster on an architecture where OCaml can - compile to native code, rather than only bytecode. At time of - writing, that is IA32, PowerPC, AMD64, Alpha, Sparc, Mips, IA64, - HPPA and StrongArm. See + Naturally, Coq will run faster on an architecture where OCaml can compile + to native code, rather than only bytecode. See http://caml.inria.fr/ocaml/portability.en.html for details. @@ -27,49 +24,36 @@ WHAT DO YOU NEED ? version suits you, follow the usual procedure for your OS to install it. E.g.: - - Debian GNU/Linux (or Debian GNU/k*BSD or ...): + - Debian GNU/Linux derivatives (or Debian GNU/k*BSD or ...): aptitude install coq - - Gentoo GNU/Linux: + - Gentoo GNU/Linux: emerge sci-mathematics/coq - - Mandriva GNU/Linux: + - Fedora GNU/Linux: urpmi coq - Should you need or prefer to compile Coq V8.4 yourself, you need: + - MacOS: - - Objective Caml version 3.11.2 or later + port install coq + + Should you need or prefer to compile Coq V8.5 yourself, you need: + + - Objective Caml version 3.12.1 or later (available at http://caml.inria.fr/) - - Camlp5 (version <= 4.08, or 5.* transitional) + - Camlp5 (version >= 6.06) (Coq compiles with Camlp4 but might be less + well supported) - GNU Make version 3.81 or later - ( - available at http://www.gnu.org/software/make/, but also a - standard or optional add-on part to most Unices and Unix - clones, sometimes under the name "gmake". - - If a new enough version is not included in your system, nor - easily available as an add-on, this should get you a working - make: - - #Download it (wget is an example, use your favourite FTP or HTTP client) - wget http://ftp.gnu.org/pub/gnu/make/make-3.81.tar.bz2 - bzip2 -cd make-3.81.tar.bz2 | tar x - #If you don't have bzip2, you can download the gzipped version instead. - cd make-3.81 - ./configure --prefix=${HOME} - make install - - Then, make sure that ${HOME}/bin is first in your $PATH. - ) - 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 + incuding gtksourceview, 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. @@ -87,31 +71,28 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.11.2 (or later) - installed on your computer and that "ocamlmktop" and "ocamlc" (or - its native code version "ocamlc.opt") lie in a directory which is present - in your $PATH environment variable. +1- Check that you have the Objective Caml compiler version 3.12.1 (or later) + installed on your computer and that "ocamlc" (or its native code version + "ocamlc.opt") lie in a directory which is present in your $PATH environment + variable. 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 Camlp4 installed on your - computer and that the command "camlp4" lies in a directory which +2- Check that you have Camlp5 (or a supported Camlp4) installed on your + computer and that the command "camlp5" lies in a directory which is present in your $PATH environment variable path. - (You need Camlp4 in both bytecode and native versions if + (You need Camlp5/4 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 +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 300 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 30 Mb, and the library about 200 Mb. 4- First you need to configure the system. It is done automatically with the command: @@ -136,7 +117,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). -libdir (default: /usr/local/lib/coq) Directory where the Coq standard library will be installed --mandir (default: /usr/local/man) +-mandir (default: /usr/local/share/man) Directory where the Coq manual pages will be installed -emacslib (default: /usr/local/lib/emacs/site-lisp) @@ -152,7 +133,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). is not necessary in that case. -opt - Use the ocamlc.opt compiler instead of ocamlc (and ocamlopt.opt + Use the ocamlc.opt compiler instead of ocamlc (and ocamlopt.opt compiler instead of ocamlopt). Makes compilation faster (recommended). -browser @@ -166,7 +147,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). to compile Coq in Objective Caml bytecode (and native-code if supported). This will compile the entire system. This phase can take more or less time, - depending on your architecture and is fairly verbose. + depending on your architecture and is fairly verbose. 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 @@ -180,7 +161,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). in you .emacs file: (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) - (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) + (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) 7- You can now clean all the sources. (You can even erase them.) @@ -190,12 +171,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). INSTALLATION PROCEDURE FOR ADVANCED USERS. ========================================== - If you wish to write tactics (and that really means that you belong - to advanced users!) 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 : + 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 @@ -218,61 +197,42 @@ THE AVAILABLE COMMANDS. ======================= There are two Coq commands: - + coqtop The Coq toplevel coqc The Coq compiler - There are actually two binaries for the interactive system, coqtop.byte - and coqtop.opt (respectively bytecode and native code versions of Coq). - coqtop is a link to the fastest version, i.e. coqtop.opt if any, and - coqtop.byte otherwise. coqc also invokes the fastest version of Coq. - Options -opt and -byte to coqtop and coqc selects a particular binary. + Under architecture where ocamlopt is available, there are actually two + binaries for the interactive system, coqtop.byte and coqtop (respectively + bytecode and native code versions of Coq). coqtop is a link to coqtop.byte + otherwise. 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. The default state - (see the "-inputstate" option) is `initial.coq', which contains some - basic logical definitions, the associated parsing and printing rules, - and the following tactic modules: Equality, Tauto, Inv, EAuto and Refine. + * `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". + 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 by FTP, 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/doc1-eng.html - - -COMMON PROBLEMS. -================ - - * On some sites, when running `./configure', `pwd' returned a - path which is not valid from another machine (it may look like - "/tmp_mnt/foo/...") and, as a consequence, you won't be able to run - coqtop or coqc. The solution is to give the correct value, with - - ./configure -src - - * The `make install' procedure uses mkdirhier, a program that may - not be present on certain systems. To fix that, try to replace - mkdirhier with mkdir -p - - * See also section on dynamically loaded libraries. + 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 : + 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; @@ -300,17 +260,16 @@ COMPILING FOR DIFFERENT ARCHITECTURES. MOVING BINARIES OR LIBRARY. =========================== - If you move the binaries or the library, Coq will be "lost". - Running "coqtop" would then return an error message of the kind: + 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: Can't find file initial.coq on loadpath + Error: cannot guess a path for Coq libraries; please use -coqlib option - 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 can then indicate the new places to Coq, using the options -coqlib : - coqtop -bindir -libdir + coqtop -coqlib See also next section. @@ -334,7 +293,7 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. the directory of the standard library of OCaml; - recompile your bytecode executables after reconfiguring the location of of the shared library: - ./configure -coqrunbyteflags "-dllib -lcoqrun -dllpath " ... + ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath," ... where is the directory where the dllcoqrun.so is installed; - (not recommended) compile bytecode executables with a custom OCaml runtime by using: -- cgit v1.2.3