From e01059f2ed199b99b291d1bd27940b0e2f9a3a0c Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 3 Nov 2000 13:16:36 +0000 Subject: compilation avec make de Solaris; README et INSTALL git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@797 85f007b7-540e-0410-9357-904b9bb8a0f7 --- INSTALL | 301 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 301 insertions(+) create mode 100644 INSTALL (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL new file mode 100644 index 000000000..44cc8c8be --- /dev/null +++ b/INSTALL @@ -0,0 +1,301 @@ + + INSTALLATION PROCEDURES FOR THE COQ V7 SYSTEM + --------------------------------------------- + +WHAT DO YOU NEED ? +================== + + Coq is designed to work on computers equipped with the Unix operating + system. In order to compile Coq V7 you need: + + - Objective Caml version 3.00 or later + (available at http://caml.inria.fr/) + + - the Camlp4 preprocessor with same version number as ocaml + (available at http://caml.inria.fr/camlp4/) + + Until now, it has mainly been tested on Sun workstations running Solaris, + and DEC alpha and Pentium workstations running Linux. By ftp, Coq + comes as a single compressed tar-file. You have probably already + decompressed it if you are reading this document. + + +QUICK INSTALLATION PROCEDURE. +============================= + +1. ./configure +2. make world +3. make install (you may need superuser rights) +4. make clean + + +INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). +================================================= + +1- Check that you have the Objective Caml compiler version 3.00 (or later) + installed on your computer and that "ocamlmktop" and "ocamlc.opt" (or + its bytecode version "ocamlc") lie in a directory which is present + in your $PATH enviroment variable. + + To get Coq in native-code, (it runs 4 to 10 times faster than + bytecode, but it takes more time to compile, uses more space), + you will also need the "ocamlopt.opt" (or its bytecode version + "ocamlopt") 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 enviroment variable path. + (You need Camlp4 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-7". 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 (about 20 Mb of disk space for the whole + system in bytecode, and 15 Mb more for native-code compilation). Once + installed, the binaries take about 14 Mb, and the library about 7 Mb. + +4- First you need to configure the system. It is done automatically with + the command: + + ./configure + + 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. + + The "configure" script accepts the following options: + +-prefix + Binaries, library, man pages and Emacs mode will be respectively + installed in /bin, /lib/coq, /man and + /lib/emacs/site-lisp + +-bindir (default: /usr/local/bin) + Directory where the binaries will be installed + +-libdir (default: /usr/local/lib/coq) + Directory where the Coq standard library will be installed + +-mandir (default: /usr/local/man) + Directory where the Coq manual pages will be installed + +-emacslib (default: /usr/local/lib/emacs/site-lisp) + Directory where the Coq Emacs mode will be installed + +-arch (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. SunOS and Solaris) + +-local + Compile Coq to run in its source directory. The installation (step 6) + is not necessary in that case. + +-opt + Use the ocamlc.opt compiler instead of ocamlc (and ocamlopt.opt + compiler instead of ocamlopt). Makes compilation faster (recommended). + +-nowarnings + Disable the Objective Caml compiler warnings. This option has no + effect on the result of the compilation. + +5- Still in the root directory, do + + make world + + 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 (about 30 minutes for both complilations + on a Pentium Pro 150), 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 + 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 "coq" "Major mode for editing Coq vernacular." t) + +7- You can now clean all the sources. (You can even erase them.) + + make cleanall + + +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 : + + ./configure -local + + Then compile the sources as described in step 5 above. The resulting + binaires will reside in the subdirectory bin/ where stands + for your architecture (usually the result of the Unix command "arch"). + Once the compilation is done, you can clean some directories with + "make clean-src" to save some disk space, the system still being usable. + + If you want to compile the sources for debugging (i.e. with the option + -g of the Caml compiler) then add the -debug option at configuration + step : + + ./configure -debug + + and then compile the sources (step 5). Then you must make a Coq toplevel + including your own tactics, which must be compiled with -g, with coqmktop. + See the chapter 16 of the Coq Reference Manual for details about how + to use coqmktop and the Objective Caml debugger with Coq. + + +UN-INSTALLATION. +================ + + Maybe one day you want to move the binaries, libaries and man pages +of Coq to another place, remove them to install a newer version, or simply +remove completely Coq from your system. + + The installation procedure (during the "make install" invocation) +produces a file COQFILES which lists all files +copied during the installation. This file is created in the Coq Library +directory, which can be easily known by typing "coqtop -where" + + To remove the binaries and the library files on a Unix system, you +just have to type : + + coqtop -uninstall + +Of course, you may need to be root to do that. + +NOTA BENE : In order not to delete others files than the coq system files, + `coqtop -uninstall' deletes only files, not directories. Maybe after + the un-installation, they are some empty directories. You can delete + them (especially /usr/local/lib/coq) by hand after having verified + that they are empty. + +THE AVAILABLE COMMANDS. +======================= + + There are two Coq commands: + + coqtop The Coq toplevel + coqc The Coq compiler + + Add option "-opt" to get Coq running natively (but then you cannot load + your own tactics dynamically -- see also option "-full") + + * `coqtop' launches Coq in the interactive mode. The default state + (see the "-inputstate" option) is `tactics.coq', which contains some + basic logical definitions, the associated parsing and printing rules, + and the following tactic modules: Tauto, ProPre, Program, Prolog and Inv. + This top-level is built on a Objective Caml top-level. From the `coqtop' + top-level, one can go to the Objective Caml top-level with the command: + + Drop. + + One goes back to Coq through the Objective Caml commands: + + #use "include.ml";; + go();; + + * `coqc' allows compilation of Coq files directly from the command line. + To compile a file foo.v, do: + + coqc foo + + It will produce a file foo.vo, that you can now load through the Coq + command "Require". + + For both coqtop and coqc the option -opt launches the native-code version, + and the option -full a native-code version with all the tactics (that is + the tactics Linear, Extraction and Natural added to the standard tactics). + + The `make world' and `make world-opt' commands create three distinct + possible input states which can be used by `coqtop': + + * tactics, which is the default state described above. + + * state, which is similar to `tactics' regarding the pre-loaded Coq + definitions, but does not load any tactic file. + + * barestate, which gives you Coq without any pre-loaded definition. It is + essentially used for compiling theories/INIT/ and thus building the + other state files. + + 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) + and in the corresponding manual pages. + + +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. T fix that, try to replace + mkdirhier with mkdir -p + +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 + + You can specify the same directory for the standard library but you + MUST specify a different directory for the binaires (of course). + + * Compile and install the system as described in steps 5 and 6 above. + + +MOVING BINARIES OR LIBRARY. +=========================== + + If you move the binaries or the library, Coq will be "lost". Usually, + running "coqtop" will then return an error message of the kind: + + Error during initialization : + Error: Can't find file tactics.coq on loadpath + + If you really have (or want) to move the binaries or the library, then + you have to tell their new places to Coq, using the options -bindir (for + the binaries directory) and -libdir (for the standard library directory) : + + coqtop -bindir -libdir + + -- cgit v1.2.3