aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-08-23 12:52:51 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-08-23 12:52:51 +0000
commit12def92b4cecdbe2fc8242bc451f4ee0d86c0eb8 (patch)
tree643aeaeee3c72ca4e3ae84440c9ac950fbdfdeb8
parent492ad5ad0b4c55610c9896436d2165ac22b527a6 (diff)
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
-rw-r--r--.gitignore1
-rw-r--r--INSTALL43
-rw-r--r--Makefile1
-rw-r--r--Makefile.build18
-rw-r--r--Makefile.common2
-rw-r--r--ide/coq.mli2
-rw-r--r--lib/envars.ml2
-rw-r--r--myocamlbuild.ml14
-rw-r--r--scripts/coqc.ml2
-rw-r--r--states/MakeInitial.v9
-rw-r--r--theories/Init/Prelude.v1
-rw-r--r--tools/coqdoc/cdglobals.ml2
-rw-r--r--toplevel/coqinit.ml4
-rw-r--r--toplevel/coqtop.ml16
-rw-r--r--toplevel/usage.ml3
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\