diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | INSTALL | 43 | ||||
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | Makefile.build | 18 | ||||
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | ide/coq.mli | 2 | ||||
| -rw-r--r-- | lib/envars.ml | 2 | ||||
| -rw-r--r-- | myocamlbuild.ml | 14 | ||||
| -rw-r--r-- | scripts/coqc.ml | 2 | ||||
| -rw-r--r-- | states/MakeInitial.v | 9 | ||||
| -rw-r--r-- | theories/Init/Prelude.v | 1 | ||||
| -rw-r--r-- | tools/coqdoc/cdglobals.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 16 | ||||
| -rw-r--r-- | toplevel/usage.ml | 3 |
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 @@ -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. @@ -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\ |