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

15 files changed, 34 insertions, 86 deletions

diff --git a/.gitignore b/.gitignore
index 1f41ade07..570342784 100644
--- a/.gitignore
+++ b/.gitignore
@@ -49,7 +49,6 @@ config/coq_config.ml
 dev/ocamldebug-coq
 plugins/micromega/csdpcert
 kernel/byterun/dllcoqrun.so
-states/initial.coq
 coqdoc.sty
 test-suite/lia.cache
 test-suite/trace
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 <command>
 	Use <command> to open an URL in a browser. %s must appear in <command>,
 	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 <correct path> <other options>
-
-    * 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 <new directory> -libdir <new directory>
+	coqtop -coqlib <new directory>
 
    See also next section.
 
diff --git a/Makefile b/Makefile
index ff345556b..ca8022cde 100644
--- a/Makefile
+++ b/Makefile
@@ -223,7 +223,6 @@ cleanconfig:
 distclean: clean cleanconfig
 
 voclean:
-	rm -f states/*.coq
 	find theories plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f
 
 devdocclean:
diff --git a/Makefile.build b/Makefile.build
index d11dcc765..37bedcf3e 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -212,7 +212,7 @@ coqlib:: theories plugins
 
 coqlight: theories-light tools coqbinaries
 
-states:: states/initial.coq
+states: theories/Init/Prelude.vo
 
 ifeq ($(BEST),opt)
 $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
@@ -471,17 +471,13 @@ btauto: $(BTAUTOVO) $(BTAUTOCMA)
 pluginsopt: $(PLUGINSOPT)
 
 ###########################################################################
-# rules to make theories, plugins and states
+# rules to make theories and plugins
 ###########################################################################
 
-states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/MakeInitial.v.d $(VO_TOOLS_ORDER_ONLY)
-	$(SHOW)'BUILD     $@'
-	$(HIDE)$(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
-
 theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY)
-	$(SHOW)'COQC -nois $<'
+	$(SHOW)'COQC -noinit $<'
 	$(HIDE)rm -f theories/Init/$*.glob
-	$(HIDE)$(BOOTCOQC) theories/Init/$* -nois
+	$(HIDE)$(BOOTCOQC) theories/Init/$* -noinit
 
 theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
 	$(OCAML) $< $(TOTARGET)
@@ -629,8 +625,6 @@ endif
 install-library:
 	$(MKDIR) $(FULLCOQLIB)
 	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
-	$(MKDIR) $(FULLCOQLIB)/states
-	$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
 	$(MKDIR) $(FULLCOQLIB)/user-contrib
 	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
 ifeq ($(BEST),opt)
@@ -647,8 +641,6 @@ endif
 install-library-light:
 	$(MKDIR) $(FULLCOQLIB)
 	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS)
-	$(MKDIR) $(FULLCOQLIB)/states
-	$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
 	rm -f $(FULLCOQLIB)/revision
 	-$(INSTALLLIB) revision $(FULLCOQLIB)
 ifeq ($(BEST),opt)
@@ -905,7 +897,7 @@ plugins/%_mod.ml: plugins/%.mllib
 	$(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@; \
 	else echo $< : Dependency $${DEPS} not ready yet; false; fi
 
-%.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
+%.vo %.glob: %.v states $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
 	$(SHOW)'COQC      $<'
 	$(HIDE)rm -f $*.glob 
 	$(HIDE)$(BOOTCOQC) $*
diff --git a/Makefile.common b/Makefile.common
index d38c6475d..a64399cd8 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -206,8 +206,6 @@ else
  PLUGINSOPT:=
 endif
 
-INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS))
-
 LINKCMO:=$(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
 
diff --git a/ide/coq.mli b/ide/coq.mli
index 9818ef661..c19fe7889 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -20,7 +20,7 @@ val version : unit -> string
 val filter_coq_opts : string list -> string list
 
 (** Launch a coqtop with the user args in order to be sure that it works,
-    checking in particular that initial.coq is found. This command
+    checking in particular that Prelude.vo is found. This command
     may terminate coqide in case of trouble *)
 val check_connection : string list -> unit
 
diff --git a/lib/envars.ml b/lib/envars.ml
index 0fd55d3fc..b4c72b130 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -82,7 +82,7 @@ let reldir instdir testfile oth =
   if Sys.file_exists (Filename.concat out testfile) then out else oth ()
 
 let guess_coqlib fail =
-  let file = "states/initial.coq" in
+  let file = "theories/Init/Prelude.vo" in
     reldir (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) file
       (fun () ->
         let coqlib = match Coq_config.coqlib with
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 1b239ee91..9bfe6995a 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -126,9 +126,7 @@ let copcodes = "kernel/copcodes.ml"
 
 let libcoqrun = "kernel/byterun/libcoqrun.a"
 
-let initialcoq = "states/initial.coq"
-let init_vo = ["theories/Init/Prelude.vo";"theories/Init/Logic_Type.vo"]
-let makeinitial = "states/MakeInitial.v"
+let init_vo = "theories/Init/Prelude.vo"
 
 let nmake = "theories/Numbers/Natural/BigN/NMake_gen.v"
 let nmakegen = "theories/Numbers/Natural/BigN/NMake_gen.ml"
@@ -447,8 +445,8 @@ let extra_rules () = begin
   in
 
   let coq_v_rule d init =
-    let bootflag = if init then A"-nois" else N in
-    let gendep = if init then coqtopbest else initialcoq in
+    let bootflag = if init then A"-noinit" else N in
+    let gendep = if init then coqtopbest else init_vo in
     rule (d^".v.vo")
       ~prods:[d^"%.vo";d^"%.glob"] ~deps:[gendep;d^"%.v";d^"%.v.depends"]
       (fun env build ->
@@ -459,12 +457,6 @@ let extra_rules () = begin
   coq_v_rule "theories/Init/" true;
   coq_v_rule "" false;
 
-(** Initial state *)
-
-  rule "initial.coq" ~prod:initialcoq ~deps:(makeinitial::init_vo)
-    (cmd [P coqtopbest;A"-boot";A"-batch";A"-nois";A"-notop";A"-silent";
-	  A"-l";P makeinitial; A"-outputstate";Px initialcoq]);
-
 (** Generation of _plugin_mod.ml files *)
 
   rule "_mod.ml" ~prod:"%_plugin_mod.ml" ~dep:"%_plugin.mllib"
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 0a3938ae1..9b2054400 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -140,7 +140,7 @@ let parse_args () =
     | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
 
     | ("-notactics"|"-debug"|"-nolib"|"-boot"
-      |"-batch"|"-nois"|"-noglob"|"-no-glob"
+      |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
       |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
diff --git a/states/MakeInitial.v b/states/MakeInitial.v
deleted file mode 100644
index 109e0c305..000000000
--- a/states/MakeInitial.v
+++ /dev/null
@@ -1,9 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-Require Export Prelude.
-Require Export Logic_Type.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 92b0dcfc1..3fa62e0a4 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -8,6 +8,7 @@
 
 Require Export Notations.
 Require Export Logic.
+Require Export Logic_Type.
 Require Export Datatypes.
 Require Export Specif.
 Require Export Peano.
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index f37db46b4..070778fb2 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -71,7 +71,7 @@ let normalize_filename f =
 (** A weaker analog of the function in Envars *)
 
 let guess_coqlib () =
-  let file = "states/initial.coq" in
+  let file = "theories/Init/Prelude.vo" in
   match Coq_config.coqlib with
     | Some coqlib when Sys.file_exists (Filename.concat coqlib file) ->
       coqlib
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 11c082e12..eac009984 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -96,7 +96,7 @@ let init_load_path () =
   let user_contrib = coqlib/"user-contrib" in
   let xdg_dirs = Envars.xdg_dirs (fun x -> msg_warning (str x)) in
   let coqpath = Envars.coqpath in
-  let dirs = ["states";"plugins"] in
+  let dirs = ["plugins"] in
     (* NOTE: These directories are searched from last to first *)
     (* first, developer specific directory to open *)
     if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
@@ -104,7 +104,7 @@ let init_load_path () =
     List.iter
       (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root]))
       theories_dirs_map;
-    (* then states and plugins *)
+    (* then plugins *)
     List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
     (* then user-contrib *)
     if Sys.file_exists user_contrib then
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f76558911..cd7da30bb 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -63,13 +63,9 @@ let unset_toplevel_name () = toplevel_name := None
 
 let remove_top_ml () = Mltop.remove ()
 
-let inputstate = ref None
-let set_inputstate s = inputstate:= Some s
-let inputstate () =
-  match !inputstate with
-    | Some "" -> ()
-    | Some s -> intern_state s
-    | None -> intern_state "initial.coq"
+let inputstate = ref ""
+let set_inputstate s = inputstate:=s
+let inputstate () = if !inputstate <> "" then intern_state !inputstate
 
 let outputstate = ref ""
 let set_outputstate s = outputstate:=s
@@ -101,11 +97,13 @@ let load_vernac_obj () =
   List.iter (fun f -> Library.require_library_from_file None f None)
     (List.rev !load_vernacular_obj)
 
+let load_init = ref true
+
 let require_list = ref ([] : string list)
 let add_require s = require_list := s :: !require_list
 let require () =
   List.iter (fun s -> Library.require_library_from_file None s (Some false))
-    (List.rev !require_list)
+    ((if !load_init then ["Prelude"] else []) @ List.rev !require_list)
 
 let compile_list = ref ([] : (bool * string) list)
 let add_compile verbose s =
@@ -196,7 +194,7 @@ let parse_args arglist =
       Flags.load_proofs := Flags.Force; set_outputstate s; parse rem
     | "-outputstate" :: []       -> usage ()
 
-    | "-nois" :: rem -> set_inputstate ""; parse rem
+    | ("-noinit"|"-nois") :: rem -> load_init := false; parse rem
 
     | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem
     | ("-inputstate"|"-is") :: []       -> usage ()
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 2ddd42d7b..4751f7e32 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -27,9 +27,10 @@ let print_usage_channel co command =
 \n  -notop                 set the toplevel name to be the empty logical path\
 \n  -exclude-dir f         exclude subdirectories named f for option -R\
 \n\
+\n  -noinit                start without loading the Init library\
+\n  -nois                  (idem)\
 \n  -inputstate f          read state from file f.coq\
 \n  -is f                  (idem)\
-\n  -nois                  start with an empty state\
 \n  -outputstate f         write state in file f.coq\
 \n  -compat X.Y            provides compatibility support for Coq version X.Y\
 \n  -verbose-compat-notations  be warned when using compatibility notations\