From 12def92b4cecdbe2fc8242bc451f4ee0d86c0eb8 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 23 Aug 2012 12:52:51 +0000 Subject: No more states/initial.coq, instead coqtop now requires Prelude.vo For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7 --- INSTALL | 43 ++++++++++--------------------------------- 1 file changed, 10 insertions(+), 33 deletions(-) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index 674d5e25d..a868f8fc8 100644 --- a/INSTALL +++ b/INSTALL @@ -69,7 +69,8 @@ WHAT DO YOU NEED ? - 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. @@ -155,10 +156,6 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). 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. - -browser Use to open an URL in a browser. %s must appear in , and will be replaced by the URL. @@ -232,10 +229,8 @@ THE AVAILABLE COMMANDS. 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: @@ -253,23 +248,6 @@ THE AVAILABLE COMMANDS. 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. - - COMPILING FOR DIFFERENT ARCHITECTURES. ====================================== @@ -304,17 +282,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. -- cgit v1.2.3