diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-03 13:16:36 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-03 13:16:36 +0000 |
| commit | e01059f2ed199b99b291d1bd27940b0e2f9a3a0c (patch) | |
| tree | 15bc3d6f8208271f633f49c25a3d808205290f8f | |
| parent | 2ee3db6e70ad47bf128163f0aa1570f7316c540a (diff) | |
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
| -rw-r--r-- | .depend | 138 | ||||
| -rw-r--r-- | INSTALL | 301 | ||||
| -rw-r--r-- | Makefile | 37 | ||||
| -rw-r--r-- | README | 83 | ||||
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | toplevel/.cvsignore | 3 |
6 files changed, 487 insertions, 77 deletions
@@ -644,27 +644,29 @@ proofs/clenv.cmx: kernel/environ.cmx kernel/evd.cmx kernel/instantiate.cmx \ kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx \ lib/util.cmx proofs/clenv.cmi proofs/evar_refiner.cmo: parsing/astterm.cmi kernel/environ.cmi \ - kernel/evd.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \ - proofs/refiner.cmi lib/stamps.cmi kernel/term.cmi pretyping/typing.cmi \ - lib/util.cmi proofs/evar_refiner.cmi + pretyping/evarutil.cmi kernel/evd.cmi library/global.cmi proofs/logic.cmi \ + kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi lib/stamps.cmi \ + kernel/term.cmi pretyping/typing.cmi lib/util.cmi proofs/evar_refiner.cmi proofs/evar_refiner.cmx: parsing/astterm.cmx kernel/environ.cmx \ - kernel/evd.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \ - proofs/refiner.cmx lib/stamps.cmx kernel/term.cmx pretyping/typing.cmx \ - lib/util.cmx proofs/evar_refiner.cmi + pretyping/evarutil.cmx kernel/evd.cmx library/global.cmx proofs/logic.cmx \ + kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx lib/stamps.cmx \ + kernel/term.cmx pretyping/typing.cmx lib/util.cmx proofs/evar_refiner.cmi proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ - kernel/evd.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ - kernel/reduction.cmi pretyping/retyping.cmi kernel/sign.cmi \ - kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi \ - pretyping/typing.cmi lib/util.cmi proofs/logic.cmi + pretyping/evarutil.cmi kernel/evd.cmi library/global.cmi \ + kernel/inductive.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \ + pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/type_errors.cmi kernel/typeops.cmi pretyping/typing.cmi \ + lib/util.cmi proofs/logic.cmi proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \ - kernel/evd.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ - kernel/reduction.cmx pretyping/retyping.cmx kernel/sign.cmx \ - kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx \ - pretyping/typing.cmx lib/util.cmx proofs/logic.cmi + pretyping/evarutil.cmx kernel/evd.cmx library/global.cmx \ + kernel/inductive.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \ + pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/type_errors.cmx kernel/typeops.cmx pretyping/typing.cmx \ + lib/util.cmx proofs/logic.cmi proofs/macros.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi proofs/proof_type.cmi library/summary.cmi \ @@ -684,15 +686,17 @@ proofs/pfedit.cmx: parsing/astterm.cmx kernel/declarations.cmx \ proofs/proof_type.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \ pretyping/typing.cmx lib/util.cmx proofs/pfedit.cmi proofs/proof_trees.cmo: parsing/ast.cmi pretyping/detyping.cmi \ - kernel/environ.cmi kernel/evd.cmi library/global.cmi kernel/names.cmi \ - lib/pp.cmi parsing/pretty.cmi parsing/printer.cmi proofs/proof_type.cmi \ - kernel/sign.cmi lib/stamps.cmi kernel/term.cmi parsing/termast.cmi \ - pretyping/typing.cmi lib/util.cmi proofs/proof_trees.cmi + kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \ + library/global.cmi kernel/names.cmi lib/pp.cmi parsing/pretty.cmi \ + parsing/printer.cmi proofs/proof_type.cmi kernel/sign.cmi lib/stamps.cmi \ + kernel/term.cmi parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \ + proofs/proof_trees.cmi proofs/proof_trees.cmx: parsing/ast.cmx pretyping/detyping.cmx \ - kernel/environ.cmx kernel/evd.cmx library/global.cmx kernel/names.cmx \ - lib/pp.cmx parsing/pretty.cmx parsing/printer.cmx proofs/proof_type.cmx \ - kernel/sign.cmx lib/stamps.cmx kernel/term.cmx parsing/termast.cmx \ - pretyping/typing.cmx lib/util.cmx proofs/proof_trees.cmi + kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \ + library/global.cmx kernel/names.cmx lib/pp.cmx parsing/pretty.cmx \ + parsing/printer.cmx proofs/proof_type.cmx kernel/sign.cmx lib/stamps.cmx \ + kernel/term.cmx parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \ + proofs/proof_trees.cmi proofs/proof_type.cmo: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi \ lib/util.cmi proofs/proof_type.cmi @@ -730,19 +734,19 @@ proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \ proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \ kernel/term.cmx pretyping/typing.cmx lib/util.cmx proofs/tacinterp.cmi proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi library/declare.cmi \ - kernel/environ.cmi proofs/evar_refiner.cmi kernel/evd.cmi \ - kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ - kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi lib/stamps.cmi \ - pretyping/tacred.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ - proofs/tacmach.cmi + kernel/environ.cmi proofs/evar_refiner.cmi pretyping/evarutil.cmi \ + kernel/evd.cmi library/global.cmi kernel/instantiate.cmi proofs/logic.cmi \ + kernel/names.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi kernel/reduction.cmi proofs/refiner.cmi \ + kernel/sign.cmi lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi \ + pretyping/typing.cmi lib/util.cmi proofs/tacmach.cmi proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx library/declare.cmx \ - kernel/environ.cmx proofs/evar_refiner.cmx kernel/evd.cmx \ - kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ - kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx lib/stamps.cmx \ - pretyping/tacred.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ - proofs/tacmach.cmi + kernel/environ.cmx proofs/evar_refiner.cmx pretyping/evarutil.cmx \ + kernel/evd.cmx library/global.cmx kernel/instantiate.cmx proofs/logic.cmx \ + kernel/names.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx kernel/reduction.cmx proofs/refiner.cmx \ + kernel/sign.cmx lib/stamps.cmx pretyping/tacred.cmx kernel/term.cmx \ + pretyping/typing.cmx lib/util.cmx proofs/tacmach.cmi proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi parsing/printer.cmi \ proofs/proof_trees.cmi proofs/tacmach.cmi proofs/tactic_debug.cmi proofs/tactic_debug.cmx: parsing/ast.cmx lib/pp.cmx parsing/printer.cmx \ @@ -905,14 +909,14 @@ tactics/tacentries.cmx: proofs/proof_trees.cmx proofs/tacmach.cmx \ tactics/tacticals.cmx tactics/tactics.cmx tactics/tacentries.cmi tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ - kernel/evd.cmi library/global.cmi library/indrec.cmi kernel/inductive.cmi \ + library/global.cmi library/indrec.cmi kernel/inductive.cmi \ kernel/names.cmi parsing/pattern.cmi lib/pp.cmi parsing/pretty.cmi \ kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi proofs/tacinterp.cmi \ proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \ tactics/wcclausenv.cmi tactics/tacticals.cmi tactics/tacticals.cmx: proofs/clenv.cmx parsing/coqast.cmx \ kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ - kernel/evd.cmx library/global.cmx library/indrec.cmx kernel/inductive.cmx \ + library/global.cmx library/indrec.cmx kernel/inductive.cmx \ kernel/names.cmx parsing/pattern.cmx lib/pp.cmx parsing/pretty.cmx \ kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \ proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \ @@ -975,7 +979,7 @@ toplevel/coqinit.cmo: config/coq_config.cmi library/library.cmi \ toplevel/mltop.cmi lib/options.cmi lib/pp.cmi lib/system.cmi \ toplevel/toplevel.cmi toplevel/vernac.cmi toplevel/coqinit.cmi toplevel/coqinit.cmx: config/coq_config.cmx library/library.cmx \ - toplevel/mltop.cmi lib/options.cmx lib/pp.cmx lib/system.cmx \ + toplevel/mltop.cmx lib/options.cmx lib/pp.cmx lib/system.cmx \ toplevel/toplevel.cmx toplevel/vernac.cmx toplevel/coqinit.cmi toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \ toplevel/errors.cmi library/lib.cmi library/library.cmi \ @@ -984,7 +988,7 @@ toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \ toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi toplevel/coqtop.cmi toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \ toplevel/errors.cmx library/lib.cmx library/library.cmx \ - toplevel/mltop.cmi lib/options.cmx lib/pp.cmx lib/profile.cmx \ + toplevel/mltop.cmx lib/options.cmx lib/pp.cmx lib/profile.cmx \ library/states.cmx lib/system.cmx toplevel/toplevel.cmx \ toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx toplevel/coqtop.cmi toplevel/discharge.cmo: pretyping/class.cmi pretyping/classops.cmi \ @@ -1045,6 +1049,12 @@ toplevel/minicoq.cmx: kernel/declarations.cmx toplevel/fhimsg.cmx \ parsing/g_minicoq.cmi kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \ kernel/safe_typing.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx lib/util.cmx +toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \ + lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi toplevel/mltop.cmi +toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \ + lib/pp.cmx library/summary.cmx lib/system.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx toplevel/mltop.cmi toplevel/protectedtoplevel.cmo: toplevel/errors.cmi parsing/pcoq.cmi \ lib/pp.cmi toplevel/vernac.cmi toplevel/vernacinterp.cmi \ toplevel/protectedtoplevel.cmi @@ -1067,7 +1077,7 @@ toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi toplevel/mltop.cmi \ kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \ lib/pp.cmi toplevel/protectedtoplevel.cmi lib/util.cmi \ toplevel/vernac.cmi toplevel/vernacinterp.cmi toplevel/toplevel.cmi -toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \ +toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmx \ kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \ lib/pp.cmx toplevel/protectedtoplevel.cmx lib/util.cmx \ toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi @@ -1084,30 +1094,32 @@ toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ pretyping/class.cmi toplevel/command.cmi parsing/coqast.cmi \ library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \ - kernel/evd.cmi parsing/extend.cmi library/global.cmi library/goptions.cmi \ - library/impargs.cmi library/lib.cmi library/libobject.cmi \ - library/library.cmi toplevel/metasyntax.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \ - lib/pp_control.cmi parsing/pretty.cmi parsing/printer.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \ - kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi library/states.cmi \ - lib/system.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ - pretyping/tacred.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \ - kernel/term.cmi kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + pretyping/evarutil.cmi kernel/evd.cmi parsing/extend.cmi \ + library/global.cmi library/goptions.cmi library/impargs.cmi \ + library/lib.cmi library/libobject.cmi library/library.cmi \ + toplevel/metasyntax.cmi kernel/names.cmi library/nametab.cmi \ + lib/options.cmi proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi \ + parsing/pretty.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi toplevel/record.cmi kernel/reduction.cmi \ + proofs/refiner.cmi lib/stamps.cmi library/states.cmi lib/system.cmi \ + proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ + proofs/tactic_debug.cmi tactics/tactics.cmi kernel/term.cmi \ + kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ toplevel/vernacentries.cmi toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ pretyping/class.cmx toplevel/command.cmx parsing/coqast.cmx \ library/declare.cmx toplevel/discharge.cmx kernel/environ.cmx \ - kernel/evd.cmx parsing/extend.cmx library/global.cmx library/goptions.cmx \ - library/impargs.cmx library/lib.cmx library/libobject.cmx \ - library/library.cmx toplevel/metasyntax.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \ - lib/pp_control.cmx parsing/pretty.cmx parsing/printer.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \ - kernel/reduction.cmx proofs/refiner.cmx lib/stamps.cmx library/states.cmx \ - lib/system.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ - pretyping/tacred.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \ - kernel/term.cmx kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + pretyping/evarutil.cmx kernel/evd.cmx parsing/extend.cmx \ + library/global.cmx library/goptions.cmx library/impargs.cmx \ + library/lib.cmx library/libobject.cmx library/library.cmx \ + toplevel/metasyntax.cmx kernel/names.cmx library/nametab.cmx \ + lib/options.cmx proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx \ + parsing/pretty.cmx parsing/printer.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx toplevel/record.cmx kernel/reduction.cmx \ + proofs/refiner.cmx lib/stamps.cmx library/states.cmx lib/system.cmx \ + proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ + proofs/tactic_debug.cmx tactics/tactics.cmx kernel/term.cmx \ + kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ toplevel/vernacentries.cmi toplevel/vernacinterp.cmo: parsing/ast.cmi toplevel/command.cmi \ parsing/coqast.cmi lib/dyn.cmi toplevel/himsg.cmi kernel/names.cmi \ 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 <options> + + 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 <dir> + Binaries, library, man pages and Emacs mode will be respectively + installed in <dir>/bin, <dir>/lib/coq, <dir>/man and + <dir>/lib/emacs/site-lisp + +-bindir <dir> (default: /usr/local/bin) + Directory where the binaries will be installed + +-libdir <dir> (default: /usr/local/lib/coq) + Directory where the Coq standard library will be installed + +-mandir <dir> (default: /usr/local/man) + Directory where the Coq manual pages will be installed + +-emacslib <dir> (default: /usr/local/lib/emacs/site-lisp) + Directory where the Coq Emacs mode will be installed + +-arch <value> (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 <other options> + + Then compile the sources as described in step 5 above. The resulting + binaires will reside in the subdirectory bin/<arch> where <arch> 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 <other options> + + 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 <correct path> <other options> + + * 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 <options> + + 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 <new directory> -libdir <new directory> + + @@ -53,8 +53,6 @@ COQINCLUDES=-I contrib/omega -I contrib/ring -I contrib/xml \ # Objects files ########################################################################### -STRLIB=-cclib -lstr - CLIBS=unix.cma CAMLP4OBJS=gramlib.cma @@ -162,7 +160,7 @@ COQMKTOPCMO=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo $(COQMKTOP): $(COQMKTOPCMO) $(OCAMLC) $(BYTEFLAGS) -o $(COQMKTOP) -custom str.cma unix.cma \ - $(COQMKTOPCMO) $(OSDEPLIBS) $(STRLIB) + $(COQMKTOPCMO) $(OSDEPLIBS) scripts/tolink.ml: Makefile echo "let lib = \""$(LIB)"\"" > $@ @@ -363,8 +361,7 @@ tools/coq_makefile: tools/coq_makefile.ml $(OCAMLOPT) $(OPTFLAGS) -o tools/coq_makefile tools/coq_makefile.ml tools/coq-tex: tools/coq-tex.ml - $(OCAMLOPT) $(OPTFLAGS) -o tools/coq-tex str.cmxa tools/coq-tex.ml \ - $(STRLIB) + $(OCAMLOPT) $(OPTFLAGS) -o tools/coq-tex str.cmxa tools/coq-tex.ml archclean:: rm -f tools/coqdep tools/gallina tools/coq-tex tools/coq_makefile @@ -399,7 +396,10 @@ install-binaries: cp tools/coqdep tools/gallina tools/coq_makefile tools/coq-tex \ $(BINDIR) +ALLVO=$(INITVO) $(TACTICSVO) $(THEORIESVO) $(CONTRIBVO) + install-library: + cp $(ALLVO) $(COQLIB) cp tools/coq.el tools/coq.elc $(EMACSLIB) MANPAGES=tools/coq-tex.1 tools/coqdep.1 tools/gallina.1 @@ -415,7 +415,7 @@ install-manpages: .PHONY: doc doc: doc/coq.tex - make -C doc coq.ps minicoq.dvi + $(MAKE) -C doc coq.ps minicoq.dvi LPLIB = lib/doc.tex $(LIB:.cmo=.mli) LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli) @@ -491,15 +491,26 @@ beforedepend:: parsing/pcoq.ml parsing/extend.ml # toplevel/mltop.ml4 (ifdef Byte) +toplevel/mltop.cmo: toplevel/mltop.byteml + $(OCAMLC) $(BYTEFLAGS) -c -impl toplevel/mltop.byteml -o $@ + +toplevel/mltop.cmx: toplevel/mltop.optml + $(OCAMLOPT) $(OPTFLAGS) -c -impl toplevel/mltop.optml -o $@ + +toplevel/mltop.byteml: toplevel/mltop.ml4 + $(CAMLP4O) pr_o.cmo pa_ifdef.cmo -DByte -impl toplevel/mltop.ml4 > $@ || rm -f $@ + +toplevel/mltop.optml: toplevel/mltop.ml4 + $(CAMLP4O) pr_o.cmo pa_ifdef.cmo -impl toplevel/mltop.ml4 > $@ || rm -f $@ + toplevel/mltop.ml: toplevel/mltop.ml4 - $(CAMLP4O) pr_o.cmo pa_ifdef.cmo -DByte -impl $< > $@ || rm -f $@ -toplevel/mltop.cmo: toplevel/mltop.ml4 - $(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) pa_ifdef.cmo -DByte -impl" \ - -c -impl $< -toplevel/mltop.cmx: toplevel/mltop.ml4 - $(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) pa_ifdef.cmo -impl" -c -impl $< + $(CAMLP4O) pr_o.cmo pa_ifdef.cmo -DByte -impl toplevel/mltop.ml4 > $@ || rm -f $@ + ML4FILES += toplevel/mltop.ml4 +clean:: + rm -f toplevel/mltop.ml toplevel/mltop.byteml toplevel/mltop.optml + ########################################################################### # Default rules ########################################################################### @@ -590,7 +601,7 @@ ML4FILESML = $(ML4FILES:.ml4=.ml) dependcamlp4: beforedepend $(ML4FILESML) ocamldep $(DEPFLAGS) $(ML4FILESML) > .depend.camlp4 for f in $(ML4FILES); do \ - echo -n `dirname $$f`/`basename $$f .ml4`".ml: " >> .depend.camlp4; \ + printf "%s" `dirname $$f`/`basename $$f .ml4`".ml: " >> .depend.camlp4; \ echo `$(CAMLP4DEPS) $$f` >> .depend.camlp4; \ done rm -f toplevel/mltop.ml @@ -0,0 +1,83 @@ + + THE COQ V7 SYSTEM + ================= + +INSTALLATION. +============= + + See the file INSTALL for installation procedure. + + +DOCUMENTATION. +============== + + The documentation of Coq V7 is available by anonymous ftp (see below), + in a directory doc/. The documents are available separately or + all together in the tar file all-docs.tar . + + +CHANGES. +======== + + There is a file named CHANGES that explains the differences and the + incompatibilities since last versions. If you upgrade Coq, please read + it carefully. + + +AVAILABILITY. +============= + + Coq is available by anonymous FTP on ftp.inria.fr: + + host: ftp.inria.fr (192.93.2.54) + directory: INRIA/coq/ + +THE COQ CLUB. +============= + + The Coq Club moderated mailing list is meant to be a standard way to + discuss questions about the Coq system and related topics. The submission + address is: + + coq-club@margaux.inria.fr + + The topics to be discussed in the club should include: + + * technical problems; + + * questions about proof developments; + + * suggestions and questions about the implementation; + + * announcements of proofs; + + * theoretical questions about typed lambda-calculi which are + closely related to Coq. + + To be added to, or removed from, the mailing list, please write to: + + coq-club-request@margaux.inria.fr + + Please use also this address for any questions/suggestions about the + Coq Club. It might sometimes take a few days before your messages get + forwarded. + + +BUGS REPORT. +============ + + Send your bug reports by E-mail to + + coq@pauillac.inria.fr + + or by snail mail to + + Projet Coq + INRIA Rocquencourt + B.P. 105 + 78153 Le Chesnay + France + + 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. @@ -8,7 +8,7 @@ VERSION=7.00 VERSIONSI=1.0 -DATE="December 1999" +DATE="November 2000" # a local which command for sh which () { diff --git a/toplevel/.cvsignore b/toplevel/.cvsignore new file mode 100644 index 000000000..0851e5725 --- /dev/null +++ b/toplevel/.cvsignore @@ -0,0 +1,3 @@ +mltop.ml +mltop.byteml +mltop.optml |