Permalink
Browse files

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
  • Loading branch information...
1 parent 492ad5a commit 12def92b4cecdbe2fc8242bc451f4ee0d86c0eb8 letouzey committed Aug 23, 2012
Showing with 34 additions and 86 deletions.
  1. +0 −1 .gitignore
  2. +10 −33 INSTALL
  3. +0 −1 Makefile
  4. +5 −13 Makefile.build
  5. +0 −2 Makefile.common
  6. +1 −1 ide/coq.mli
  7. +1 −1 lib/envars.ml
  8. +3 −11 myocamlbuild.ml
  9. +1 −1 scripts/coqc.ml
  10. +0 −9 states/MakeInitial.v
  11. +1 −0 theories/Init/Prelude.v
  12. +1 −1 tools/coqdoc/cdglobals.ml
  13. +2 −2 toplevel/coqinit.ml
  14. +7 −9 toplevel/coqtop.ml
  15. +2 −1 toplevel/usage.ml
View
@@ -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
View
43 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.
View
@@ -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:
View
@@ -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) $*
View
@@ -206,8 +206,6 @@ else
PLUGINSOPT:=
endif
-INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS))
-
LINKCMO:=$(CORECMA) $(STATICPLUGINS)
LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
View
@@ -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
View
@@ -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
View
@@ -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"
View
@@ -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"
View
@@ -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.
View
@@ -8,6 +8,7 @@
Require Export Notations.
Require Export Logic.
+Require Export Logic_Type.
Require Export Datatypes.
Require Export Specif.
Require Export Peano.
@@ -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
View
@@ -96,15 +96,15 @@ 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";
(* then standard library *)
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
View
@@ -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 ()
View
@@ -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\

0 comments on commit 12def92

Please sign in to comment.