diff options
129 files changed, 1835 insertions, 1422 deletions
diff --git a/.dir-locals.el b/.dir-locals.el deleted file mode 100644 index e32ce14a4..000000000 --- a/.dir-locals.el +++ /dev/null @@ -1,37 +0,0 @@ -;; EMACS CONFIGURATION FOR COQ DEVELOPPERS This configuration will be -;; executed for each opened file under coq root directory. -((nil - . ((eval - . (progn - ;; coq root directory (ending with slash) - (let ((coq-root-directory (when buffer-file-name - (locate-dominating-file - buffer-file-name - ".dir-locals.el"))) - (coq-project-find-file - (and (boundp 'coq-project-find-file) coq-project-find-file))) - ;; coq tags file and coq debugger executable - (set (make-local-variable 'tags-file-name) - (concat coq-root-directory "TAGS")) - (setq camldebug-command-name (concat coq-root-directory - "dev/ocamldebug-coq")) - - ;; Setting the compilation directory to coq root. This is - ;; mutually exclusive with the setting of default-directory - ;; below. Also setting the path for next error. - (unless coq-project-find-file - (set (make-local-variable 'compile-command) - (concat "make -C " coq-root-directory)) - (set (make-local-variable 'compilation-search-path) - (cons coq-root-directory nil))) - - ;; Set default directory to coq root ONLY IF variable - ;; coq-project-find-file is non nil. This should remain a - ;; user preference and not be set by default. This setting - ;; is redundant with compile-command above as M-x compile - ;; always CD's to default directory. To enable it add this - ;; to your emacs config: (setq coq-project-find-file t) - (when coq-project-find-file - (setq default-directory coq-root-directory)))) - )) - )) diff --git a/.gitignore b/.gitignore index 1e7f982a5..b857b754a 100644 --- a/.gitignore +++ b/.gitignore @@ -55,7 +55,7 @@ config/Makefile config/coq_config.ml config/Info-*.plist dev/ocamldebug-coq -dev/camlp4.dbg +dev/camlp5.dbg plugins/micromega/csdpcert plugins/micromega/.micromega.ml.generated kernel/byterun/dllcoqrun.so @@ -68,6 +68,11 @@ Universes module and library boundaries. Global universe names introduced in an inductive / constant / Let declaration get qualified with the name of the declaration. +- Universe cumulativity for inductive types is now specified as a + variance for each polymorphic universe. See the reference manual for + more information. +- Fix #5726: Notations that start with `Type` now support universe instances + with `@{u}`. Checker @@ -84,6 +89,18 @@ Documentation moved to the GitHub wiki section of this repository; the main entry page is https://github.com/coq/coq/wiki/The-Coq-FAQ. +Changes from 8.7.1 to 8.7.2 +=========================== + +Fixed a critical bug in the VM handling of universes (#6677). This bug +affected all releases since 8.5. + +Improved support for building with OCaml 4.06.0 and external num package. + +Many other bug fixes, documentation improvements, and user +message improvements (for details, see the 8.7.2 milestone at +https://github.com/coq/coq/milestone/11?closed=1). + Changes from 8.7.0 to 8.7.1 =========================== @@ -266,7 +266,7 @@ cacheclean: find theories plugins test-suite -name '.*.aux' -delete cleanconfig: - rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp4.dbg config/Info-*.plist + rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist distclean: clean cleanconfig cacheclean timingclean diff --git a/Makefile.build b/Makefile.build index f0dd46b0f..39d177a13 100644 --- a/Makefile.build +++ b/Makefile.build @@ -196,7 +196,7 @@ COQOPTS=$(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) -MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) +MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP5LIB) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) @@ -240,8 +240,8 @@ endef # Camlp5 settings -CAMLP4DEPS:=grammar/grammar.cma -CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) +CAMLP5DEPS:=grammar/grammar.cma +CAMLP5USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) @@ -345,14 +345,14 @@ grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \ ## Ocaml compiler with the right options and -I for grammar GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \ - -I $(MYCAMLP4LIB) -I grammar + -I $(MYCAMLP5LIB) -I grammar ## Specific rules for grammar.cma grammar/grammar.cma : $(GRAMCMO) $(SHOW)'Testing $@' @touch grammar/test.mlp - $(HIDE)$(GRAMC) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test + $(HIDE)$(GRAMC) -pp '$(CAMLP5O) -I $(MYCAMLP5LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test @rm -f grammar/test.* grammar/test $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -a -o $@ @@ -361,7 +361,7 @@ grammar/grammar.cma : $(GRAMCMO) COMPATCMO:= GRAMP4USE:=$(COMPATCMO) pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) -GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl +GRAMPP:=$(CAMLP5O) -I $(MYCAMLP5LIB) $(GRAMP4USE) $(CAMLP5COMPAT) -impl ## Rules for standard .mlp and .mli files in grammar/ @@ -406,17 +406,16 @@ $(COQTOPEXE): $(COQTOPBYTE) cp $< $@ endif -# Are "-cclib lcoqrun -dllib -lcoqrun" necessary? +# VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM $(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \ - -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \ + -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ $(LINKCMO) $(BYTEFLAGS) \ $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@ -# coqc - +# For coqc COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo $(COQC): $(call bestobj, $(COQCCMO)) @@ -684,10 +683,10 @@ plugins/%.cmx: plugins/%.ml $(SHOW)'OCAMLLEX $<' $(HIDE)$(OCAMLLEX) -o $@ "$*.mll" -%.ml: %.ml4 $(CAMLP4DEPS) +%.ml: %.ml4 $(CAMLP5DEPS) $(SHOW)'CAMLP5O $<' - $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) \ - $(CAMLP4DEPS) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@ + $(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \ + $(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@ ########################################################################### diff --git a/Makefile.ci b/Makefile.ci index 334827a93..80fbd7bbe 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -1,5 +1,4 @@ -CI_TARGETS=ci-all \ - ci-bignums \ +CI_TARGETS=ci-bignums \ ci-color \ ci-compcert \ ci-coq-dpdgraph \ @@ -23,7 +22,7 @@ CI_TARGETS=ci-all \ ci-unimath \ ci-vst -.PHONY: $(CI_TARGETS) +.PHONY: ci-all $(CI_TARGETS) ci-color: ci-bignums @@ -37,6 +36,8 @@ ci-formal-topology: ci-corn $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* +ci-all: $(CI_TARGETS) + # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.dev b/Makefile.dev index db83be369..d35ad7501 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -18,9 +18,9 @@ DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo devel: printers -printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp4.dbg +printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp5.dbg -dev/camlp4.dbg: +dev/camlp5.dbg: echo "load_printer gramlib.cma" > $@ ############ diff --git a/Makefile.ide b/Makefile.ide index 09eef1f6b..4846f5e60 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -106,9 +106,9 @@ $(COQIDEBYTE): $(LINKIDE) $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \ lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^ -ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ +ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp5deps here + $(SHOW)'CAMLP5O $<' + $(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) $(CAMLP5USE) -D$(IDEINT) -impl $< -o $@ ide/%.cmi: ide/%.mli diff --git a/checker/include b/checker/include index 09bf2826c..da0346359 100644 --- a/checker/include +++ b/checker/include @@ -13,7 +13,6 @@ #directory "kernel";; #directory "checker";; #directory "+threads";; -#directory "+camlp4";; #directory "+camlp5";; #load "unix.cma";; diff --git a/config/coq_config.mli b/config/coq_config.mli index e2d9d0d01..5f9ebdc1a 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -28,11 +28,10 @@ val ocamllex : string val camlbin : string (* base directory of OCaml binaries *) val camllib : string (* for Dynlink *) -val camlp4 : string (* exact name of camlp4: either "camlp4" ou "camlp5" *) -val camlp4o : string (* name of the camlp4o/camlp5o executable *) -val camlp4bin : string (* base directory for Camlp4/5 binaries *) -val camlp4lib : string (* where is the library of Camlp4 *) -val camlp4compat : string (* compatibility argument to camlp4/5 *) +val camlp5o : string (* name of the camlp5o executable *) +val camlp5bin : string (* base directory for camlp5 binaries *) +val camlp5lib : string (* where is the library of camlp5 *) +val camlp5compat : string (* compatibility argument to camlp5 *) val coqideincl : string (* arguments for building coqide (e.g. lablgtk) *) val cflags : string (* arguments passed to gcc *) diff --git a/configure.ml b/configure.ml index 06a7dd822..9992e03b8 100644 --- a/configure.ml +++ b/configure.ml @@ -193,7 +193,7 @@ let select_command msg candidates = in search candidates (** As per bug #4828, ocamlfind on Windows/Cygwin barfs if you pass it - a quoted path to camlpXo via -pp. So we only quote camlpXo on not + a quoted path to camlp5o via -pp. So we only quote camlp5o on not Windows, and warn on Windows if the path contains spaces *) let contains_suspicious_characters str = List.fold_left (fun b ch -> String.contains str ch || b) false [' '; '\t'] @@ -487,7 +487,7 @@ let camlbin, caml_version, camllib, findlib_version = then reset_caml_top camlexec (camlbin / "ocaml") in camlbin, caml_version, camllib, findlib_version -let camlp4compat = "-loc loc" +let camlp5compat = "-loc loc" (** Caml version as a list of string, e.g. ["4";"00";"1"] *) @@ -570,9 +570,9 @@ let caml_flags = let coq_caml_flags = coq_warn_error -(** * CamlpX configuration *) +(** * Camlp5 configuration *) -(* Convention: we use camldir as a prioritary location for camlpX, if given *) +(* Convention: we use camldir as a prioritary location for camlp5, if given *) (* i.e., in the case of camlp5, we search for a copy of camlp5o which *) (* answers the right camlp5 lib dir *) @@ -588,7 +588,7 @@ let which_camlp5o_for camlp5lib = if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else die ("Error: cannot find Camlp5 binaries corresponding to Camlp5 library " ^ camlp5lib) -let which_camlpX base = +let which_camlp5 base = let file = Filename.concat camlbin base in if is_executable file then file else which base @@ -609,7 +609,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with in die msg | None -> try - let camlp5o = which_camlpX "camlp5o" in + let camlp5o = which_camlp5 "camlp5o" in let dir,_ = tryrun camlp5o ["-where"] in dir, camlp5o with Not_found -> @@ -623,15 +623,14 @@ let check_camlp5_version camlp5o = printf "You have Camlp5 %s. Good!\n" version; version | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n" -let config_camlpX () = +let config_camlp5 () = let camlp5mod = "gramlib" in let camlp5libdir, camlp5o = check_camlp5 (camlp5mod^".cma") in let camlp5_version = check_camlp5_version camlp5o in - "camlp5", "Camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version + camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version -let camlpX, capitalized_camlpX, camlpXo, - camlpXbindir, fullcamlpXlibdir, - camlpXmod, camlpX_version = config_camlpX () +let camlp5o, camlp5bindir, fullcamlp5libdir, + camlp5mod, camlp5_version = config_camlp5 () let shorten_camllib s = if starts_with s (camllib^"/") then @@ -639,7 +638,7 @@ let shorten_camllib s = "+" ^ String.sub s l (String.length s - l) else s -let camlpXlibdir = shorten_camllib fullcamlpXlibdir +let camlp5libdir = shorten_camllib fullcamlp5libdir (** * Native compiler *) @@ -649,8 +648,8 @@ let msg_byteonly () = let msg_no_ocamlopt () = printf "Cannot find the OCaml native-code compiler.\n"; msg_byteonly () -let msg_no_camlpX_cmxa () = - printf "Cannot find the native-code library of %s.\n" camlpX; msg_byteonly () +let msg_no_camlp5_cmxa () = + printf "Cannot find the native-code library of camlp5.\n"; msg_byteonly () let msg_no_dynlink_cmxa () = printf "Cannot find native-code dynlink library.\n"; msg_byteonly (); @@ -662,8 +661,8 @@ let check_native () = let () = if !Prefs.byteonly then raise Not_found in let version, _ = tryrun camlexec.find ["opt";"-version"] in if version = "" then let () = msg_no_ocamlopt () in raise Not_found - else if not (Sys.file_exists (fullcamlpXlibdir/camlpXmod^".cmxa")) - then let () = msg_no_camlpX_cmxa () in raise Not_found + else if not (Sys.file_exists (fullcamlp5libdir/camlp5mod^".cmxa")) + then let () = msg_no_camlp5_cmxa () in raise Not_found else if fst (tryrun camlexec.find ["query";"dynlink"]) = "" then let () = msg_no_dynlink_cmxa () in raise Not_found else @@ -1015,9 +1014,9 @@ let print_summary () = pr " OCaml binaries in : %s\n" (esc camlbin); pr " OCaml library in : %s\n" (esc camllib); pr " OCaml flambda flags : %s\n" (String.concat " " !Prefs.flambda_flags); - pr " %s version : %s\n" capitalized_camlpX camlpX_version; - pr " %s binaries in : %s\n" capitalized_camlpX (esc camlpXbindir); - pr " %s library in : %s\n" capitalized_camlpX (esc camlpXlibdir); + pr " Camlp5 version : %s\n" camlp5_version; + pr " Camlp5 binaries in : %s\n" (esc camlp5bindir); + pr " Camlp5 library in : %s\n" (esc camlp5libdir); if best_compiler = "opt" then pr " Native dynamic link support : %B\n" hasnatdynlink; if coqide <> "no" then @@ -1057,7 +1056,7 @@ let write_dbg_wrapper f = pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure #\n\n"; pr "export COQTOP=%S\n" coqtop; pr "OCAMLDEBUG=%S\n" (camlbin^"/ocamldebug"); - pr "CAMLP4LIB=%S\n\n" camlpXlibdir; + pr "CAMLP5LIB=%S\n\n" camlp5libdir; pr ". $COQTOP/dev/ocamldebug-coq.run\n"; close_out o; Unix.chmod f 0o555 @@ -1095,11 +1094,10 @@ let write_configml f = pr_s "ocamllex" camlexec.lex; pr_s "camlbin" camlbin; pr_s "camllib" camllib; - pr_s "camlp4" camlpX; - pr_s "camlp4o" camlpXo; - pr_s "camlp4bin" camlpXbindir; - pr_s "camlp4lib" camlpXlibdir; - pr_s "camlp4compat" camlp4compat; + pr_s "camlp5o" camlp5o; + pr_s "camlp5bin" camlp5bindir; + pr_s "camlp5lib" camlp5libdir; + pr_s "camlp5compat" camlp5compat; pr_s "cflags" cflags; pr_s "caml_flags" caml_flags; pr_s "best" best_compiler; @@ -1220,12 +1218,11 @@ let write_makefile f = pr "CAMLDEBUGOPT=%s\n\n" coq_debug_flag; pr "# Compilation profile flag\n"; pr "CAMLTIMEPROF=%s\n\n" coq_profile_flag; - pr "# Camlp4 : flavor, binaries, libraries ...\n"; - pr "# NB : avoid using CAMLP4LIB (conflict under Windows)\n"; - pr "CAMLP4=%s\n" camlpX; - pr "CAMLP4O=%s\n" (win_aware_quote_executable camlpXo); - pr "CAMLP4COMPAT=%s\n" camlp4compat; - pr "MYCAMLP4LIB=%S\n\n" camlpXlibdir; + pr "# Camlp5 : flavor, binaries, libraries ...\n"; + pr "# NB : avoid using CAMLP5LIB (conflict under Windows)\n"; + pr "CAMLP5O=%s\n" (win_aware_quote_executable camlp5o); + pr "CAMLP5COMPAT=%s\n" camlp5compat; + pr "MYCAMLP5LIB=%S\n\n" camlp5libdir; pr "# Your architecture\n"; pr "# Can be obtain by UNIX command arch\n"; pr "ARCH=%s\n" arch; diff --git a/dev/README b/dev/README index 6b83579de..453f85f0d 100644 --- a/dev/README +++ b/dev/README @@ -40,7 +40,11 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) Other development tools (directory tools) ----------------------- +coqdev.el: helper customizations for everyday Coq development, eg + making `compile' work in subdirectories + objects.el: various development utilities at emacs level + anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output. diff --git a/dev/base_include b/dev/base_include index 472c0c605..350ccaa10 100644 --- a/dev/base_include +++ b/dev/base_include @@ -19,7 +19,6 @@ #directory "stm";; #directory "vernac";; -#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) #use "top_printers.ml";; @@ -230,7 +229,7 @@ let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));; -let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc) +let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqtop.drop_last_doc) let _ = print_string diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index c46767821..d8cde39f8 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -794,8 +794,8 @@ function make_ocaml { # TODO: this might not work if PREFIX contains spaces sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile - # We don't want to mess up Coq's dirctory structure so put the OCaml library in a separate folder - # If we refer to the make variable ${PREFIX} below, camlp4 ends up having a wrong path: + # We don't want to mess up Coq's directory structure so put the OCaml library in a separate folder + # If we refer to the make variable ${PREFIX} below, camlp5 ends up having the wrong path: # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4 # So we put an explicit path in there diff --git a/dev/core.dbg b/dev/core.dbg index 00a4355a4..57c136900 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -1,4 +1,4 @@ -source camlp4.dbg +source camlp5.dbg load_printer threads.cma load_printer str.cma load_printer clib.cma diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index f3fc13e96..abba13428 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -46,7 +46,7 @@ see build-system.txt . .ml4 files ---------- -.ml4 are converted to .ml by camlp4. By default, they are produced +.ml4 are converted to .ml by camlp5. By default, they are produced in the binary ast format understood by ocamlc/ocamlopt/ocamldep. Pros: - faster than parsing clear-text source file. diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 873adc1b2..1c4fd2eba 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -88,7 +88,7 @@ bootstrapped. The dependencies of a file FOO are in FOO.d . This enables partial recalculation of dependencies (only the dependencies of changed files are recomputed). -If you add a dependency to a Coq camlp4 extension (grammar.cma or +If you add a dependency to a Coq camlp5 extension (grammar.cma or q_constr.cmo), then see sections ".ml4 files" and "new files". Cleaning Targets @@ -127,7 +127,7 @@ of a grammar extension via a line of the form: The use of (*i camlp4use: ... i*) to mention uses of standard extension such as IFDEF has also been discontinued, the Makefile now -always calls camlp4 with pa_macros.cmo and a few others by default. +always calls camlp5 with pa_macros.cmo and a few others by default. For debugging a Coq grammar extension, it could be interesting to use the READABLE_ML4=1 option, otherwise the generated .ml are diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index 2dbd132da..b3d49b7e5 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -25,7 +25,7 @@ intf : grammar : - Camlp4 syntax extensions. The file grammar/grammar.cma is used + Camlp5 syntax extensions. The file grammar/grammar.cma is used to pre-process .ml4 files containing EXTEND constructions, either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND. This grammar.cma incorporates many files from other directories diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 3cbccab44..f3e60edea 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -3,19 +3,19 @@ # Wrapper around ocamldebug for Coq # This file is to be launched via the generated script ocamldebug-coq, -# which will set the env variables $OCAMLDEBUG, $CAMLP4LIB, $COQTOP +# which will set the env variables $OCAMLDEBUG, $CAMLP5LIB, $COQTOP # Anyway, just in case someone tries to use this script directly, # here are some reasonable default values [ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug -[ -z "$CAMLP4LIB" ] && CAMLP4LIB=+camlp5 +[ -z "$CAMLP5LIB" ] && CAMLP5LIB=+camlp5 [ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD [ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD` export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH exec $OCAMLDEBUG \ - -I $CAMLP4LIB -I +threads \ + -I $CAMLP5LIB -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ diff --git a/dev/tools/anomaly-traces-parser.el b/dev/tools/anomaly-traces-parser.el deleted file mode 100644 index 68f54266f..000000000 --- a/dev/tools/anomaly-traces-parser.el +++ /dev/null @@ -1,28 +0,0 @@ -;; This Elisp snippet adds a regexp parser for the format of Anomaly -;; backtraces (coqc -bt ...), to the error parser of the Compilation -;; mode (C-c C-c: "Compile command: ..."). Once the -;; coq-change-error-alist-for-backtraces function has run, file -;; locations in traces are recognized and can be jumped from easily -;; from the *compilation* buffer. - -;; You can just copy everything below to your .emacs and this will be -;; enabled from any compilation command launched from an OCaml file. - -(defun coq-change-error-alist-for-backtraces () - "Hook to change the compilation-error-regexp-alist variable, to - search the coq backtraces for error locations" - (interactive) - (add-to-list - 'compilation-error-regexp-alist-alist - '(coq-backtrace - "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ - lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\ - \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)" - 2 (3 . 4) (5 . 6))) - (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) - -;; this Anomaly parser should be available when one is hacking -;; on the *OCaml* code of Coq (adding bugs), so we enable it -;; through the OCaml mode hooks. -(add-hook 'caml-mode-hook 'coq-change-error-alist-for-backtraces) -(add-hook 'tuareg-mode-hook 'coq-change-error-alist-for-backtraces) diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index d7acf01f1..e4359f703 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -50,6 +50,15 @@ else fi +if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then + echo + read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r + echo + if [[ ! $REPLY =~ ^[Yy]$ ]]; then + exit 1 + fi +fi + if [[ "${OPTION}" == "--stop-before-merging" ]]; then exit 0 fi diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el new file mode 100644 index 000000000..8c55be283 --- /dev/null +++ b/dev/tools/coqdev.el @@ -0,0 +1,106 @@ +;;; coqdev.el --- Emacs helpers for Coq development -*- lexical-binding:t -*- + +;; Copyright (C) 2018 The Coq Development Team + +;; Maintainer: coqdev@inria.fr + +;;; Commentary: + +;; Helpers to set compilation commands, proof general variables, etc +;; for Coq development + +;; You can disable individual features without editing this file by +;; using `remove-hook', for instance +;; (remove-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) + +;;; Installation: + +;; To use this, with coqdev.el located at /path/to/coqdev.el, add the +;; following to your init: + +;; (add-to-list 'load-path "/path/to/coqdev/") +;; (require 'coqdev) + +;; If you load this file from a git repository, checking out an old +;; commit will make it disappear and cause errors for your Emacs +;; startup. To ignore those errors use (require 'coqdev nil t). If you +;; check out a malicious commit Emacs startup would allow it to run +;; arbitrary code, to avoid this you can copy coqdev.el to any +;; location and adjust the load path accordingly (of course if you run +;; ./configure to compile Coq it is already too late). + +;;; Code: + +(defun coqdev-default-directory () + "Return the Coq repository containing `default-directory'." + (let ((dir (locate-dominating-file default-directory "META.coq"))) + (when dir (expand-file-name dir)))) + +(defun coqdev-setup-compile-command () + "Setup `compile-command' for Coq development." + (let ((dir (coqdev-default-directory))) + (when dir (setq-local compile-command (concat "make -C " (shell-quote-argument dir)))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) + +(defvar camldebug-command-name) ; from camldebug.el (caml package) +(defvar ocamldebug-command-name) ; from ocamldebug.el (tuareg package) +(defun coqdev-setup-camldebug () + "Setup ocamldebug for Coq development. + +Specifically `camldebug-command-name' and `ocamldebug-command-name'." + (let ((dir (coqdev-default-directory))) + (when dir + (setq-local camldebug-command-name + (concat dir "dev/ocamldebug-coq")) + (setq-local ocamldebug-command-name + (concat dir "dev/ocamldebug-coq"))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-camldebug) + +(defun coqdev-setup-tags () + "Setup `tags-file-name' for Coq development." + (let ((dir (coqdev-default-directory))) + (when dir (setq-local tags-file-name (concat dir "TAGS"))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-tags) + +(defvar coq-prog-args) +(defvar coq-prog-name) + +;; Lets us detect whether there are file local variables +;; even though PG sets it with `setq' when there's a _Coqproject. +;; Also makes sense generally, so might make it into PG someday. +(make-variable-buffer-local 'coq-prog-args) +(setq-default coq-prog-args nil) + +(defun coqdev-setup-proofgeneral () + "Setup Proofgeneral variables for Coq development. + +Note that this function is executed before _Coqproject is read if it exists." + (let ((dir (coqdev-default-directory))) + (when dir + (unless coq-prog-args + (setq coq-prog-args + `("-coqlib" ,dir "-R" ,(concat dir "plugins") + "Coq" "-R" ,(concat dir "theories") + "Coq"))) + (setq-local coq-prog-name (concat dir "bin/coqtop"))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) + +;; This Elisp snippet adds a regexp parser for the format of Anomaly +;; backtraces (coqc -bt ...), to the error parser of the Compilation +;; mode (C-c C-c: "Compile command: ..."). File locations in traces +;; are recognized and can be jumped from easily in the *compilation* +;; buffer. +(defvar compilation-error-regexp-alist-alist) +(defvar compilation-error-regexp-alist) +(with-eval-after-load 'compile + (add-to-list + 'compilation-error-regexp-alist-alist + '(coq-backtrace + "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ + lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\ + \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)" + 2 (3 . 4) (5 . 6))) + (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) + +(provide 'coqdev) +;;; coqdev ends here diff --git a/dev/top_printers.ml b/dev/top_printers.ml index af38ce4b8..f99e2593d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -485,7 +485,7 @@ let in_current_context f c = let (evmap,sign) = Pfedit.get_current_context () in f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*) -(* We expand the result of preprocessing to be independent of camlp4 +(* We expand the result of preprocessing to be independent of camlp5 VERNAC COMMAND EXTEND PrintPureConstr | [ "PrintPureConstr" constr(c) ] -> [ in_current_context print_pure_constr c ] diff --git a/ide/coq.ml b/ide/coq.ml index 42ab86dd6..34b4875af 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -9,6 +9,8 @@ open Ideutils open Preferences +let ideslave_coqtop_flags = ref None + (** * Version and date *) let get_version_date () = @@ -375,7 +377,7 @@ let spawn_handle args respawner feedback_processor = in let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in let env = - match !Flags.ideslave_coqtop_flags with + match !ideslave_coqtop_flags with | None -> None | Some s -> let open Str in diff --git a/ide/coq.mli b/ide/coq.mli index 463dd134a..8c4727b37 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -171,3 +171,6 @@ val check_connection : string list -> unit val interrupter : (int -> unit) ref val save_all : (unit -> unit) ref + +(* Flags to be used for ideslave *) +val ideslave_coqtop_flags : string option ref diff --git a/ide/coqide.ml b/ide/coqide.ml index 3cc46b6aa..4de9a5288 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1360,7 +1360,7 @@ let read_coqide_args argv = Backtrace.record_backtrace true; filter_coqtop coqtop project_files ("-debug"::out) args |"-coqtop-flags" :: flags :: args-> - Flags.ideslave_coqtop_flags := Some flags; + Coq.ideslave_coqtop_flags := Some flags; filter_coqtop coqtop project_files out args |arg::args when out = [] && Minilib.is_prefix_of "-psn_" arg -> (* argument added by MacOS during .app launch *) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 5f40a2242..fe86df084 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -454,10 +454,13 @@ let slave_feeder fmt xml_oc msg = let msg_format = ref (fun () -> let margin = Option.default 72 (Topfmt.get_margin ()) in Xmlprotocol.Richpp margin -) + ) -let loop doc = - set_doc doc; +(* The loop ignores the command line arguments as the current model delegates + its handing to the toplevel container. *) +let loop _args ~state = + let open Vernac.State in + set_doc state.doc; init_signal_handler (); catch_break := false; let in_ch, out_ch = Spawned.get_channels () in @@ -504,8 +507,8 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let () = Coqtop.toploop_init := (fun args -> - let args = parse args in +let () = Coqtop.toploop_init := (fun coq_args extra_args -> + let args = parse extra_args in Flags.quiet := true; CoqworkmgrApi.(init High); args) diff --git a/ide/minilib.ml b/ide/minilib.ml index 2b278fac6..572222c06 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -20,7 +20,7 @@ type level = [ | `FATAL ] (** Some excerpt of Util and similar files to avoid loading the whole - module and its dependencies (and hence Compat and Camlp4) *) + module and its dependencies (and hence Compat and Camlp5) *) let debug = ref false diff --git a/ide/minilib.mli b/ide/minilib.mli index c96e59b22..4f5fbe7db 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -7,7 +7,7 @@ (***********************************************************************) (** Some excerpts of Util and similar files to avoid depending on them - and hence on Compat and Camlp4 *) + and hence on Compat and Camlp5 *) val print_list : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 9febc6449..6d91c3ec9 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -45,6 +45,55 @@ type reloc_table = (tag * int) array type annot_switch = {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} +let rec eq_structured_constant c1 c2 = match c1, c2 with +| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 +| Const_sorts _, _ -> false +| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 +| Const_ind _, _ -> false +| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 +| Const_proj _, _ -> false +| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 +| Const_b0 _, _ -> false +| Const_bn (t1, a1), Const_bn (t2, a2) -> + Int.equal t1 t2 && CArray.equal eq_structured_constant a1 a2 +| Const_bn _, _ -> false +| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 +| Const_univ_level _ , _ -> false +| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 +| Const_type _ , _ -> false + +let rec hash_structured_constant c = + let open Hashset.Combine in + match c with + | Const_sorts s -> combinesmall 1 (Sorts.hash s) + | Const_ind i -> combinesmall 2 (ind_hash i) + | Const_proj p -> combinesmall 3 (Constant.hash p) + | Const_b0 t -> combinesmall 4 (Int.hash t) + | Const_bn (t, a) -> + let fold h c = combine h (hash_structured_constant c) in + let h = Array.fold_left fold 0 a in + combinesmall 5 (combine (Int.hash t) h) + | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) + | Const_type u -> combinesmall 7 (Univ.Universe.hash u) + +let eq_annot_switch asw1 asw2 = + let eq_ci ci1 ci2 = + eq_ind ci1.ci_ind ci2.ci_ind && + Int.equal ci1.ci_npar ci2.ci_npar && + CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls + in + let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in + eq_ci asw1.ci asw2.ci && + CArray.equal eq_rlc asw1.rtbl asw2.rtbl && + (asw1.tailcall : bool) == asw2.tailcall + +let hash_annot_switch asw = + let open Hashset.Combine in + let h1 = Constr.case_info_hash asw.ci in + let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in + let h3 = if asw.tailcall then 1 else 0 in + combine3 h1 h2 h3 + module Label = struct type t = int diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 5d37a5840..bf2e462e8 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -41,6 +41,12 @@ type reloc_table = (tag * int) array type annot_switch = {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} +val eq_structured_constant : structured_constant -> structured_constant -> bool +val hash_structured_constant : structured_constant -> int + +val eq_annot_switch : annot_switch -> annot_switch -> bool +val hash_annot_switch : annot_switch -> int + module Label : sig type t = int diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 5dab2932d..4a34dbcff 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -628,27 +628,17 @@ let rec compile_constr reloc c sz cont = of the structured constant, while the later (if any) will be applied as arguments. *) let open Univ in begin - let levels = Universe.levels u in - let global_levels = - LSet.filter (fun x -> Level.var_index x = None) levels - in - let local_levels = - List.map_filter (fun x -> Level.var_index x) - (LSet.elements levels) - in + let u,s = Universe.compact u in (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) - let uglob = - LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m - in - if local_levels = [] then - compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type uglob))) sz cont + if List.is_empty s then + compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type u))) sz cont else let compile_get_univ reloc idx sz cont = set_max_stack_size sz; compile_fv_elem reloc (FVuniv_var idx) sz cont in comp_app compile_str_cst compile_get_univ reloc - (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont + (Bstrconst (Const_type u)) (Array.of_list s) sz cont end | LetIn(_,xb,_,body) -> compile_constr reloc xb sz diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index eeea19c12..856b0b465 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -10,18 +10,51 @@ machine, Oct 2004 *) (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) +open Names open Term open Cbytecodes open Copcodes open Mod_subst +type emitcodes = String.t + +external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code" + (* Relocation information *) type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant | Reloc_getglobal of Names.Constant.t -type patch = reloc_info * int +let eq_reloc_info r1 r2 = match r1, r2 with +| Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2 +| Reloc_annot _, _ -> false +| Reloc_const c1, Reloc_const c2 -> eq_structured_constant c1 c2 +| Reloc_const _, _ -> false +| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2 +| Reloc_getglobal _, _ -> false + +let hash_reloc_info r = + let open Hashset.Combine in + match r with + | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw) + | Reloc_const c -> combinesmall 2 (hash_structured_constant c) + | Reloc_getglobal c -> combinesmall 3 (Constant.hash c) + +module RelocTable = Hashtbl.Make(struct + type t = reloc_info + let equal = eq_reloc_info + let hash = hash_reloc_info +end) + +(** We use arrays for on-disk representation. On 32-bit machines, this means we + can only have a maximum amount of about 4.10^6 relocations, which seems + quite a lot, but potentially reachable if e.g. compiling big proofs. This + would prevent VM computing with these terms on 32-bit architectures. Maybe + we should use a more robust data structure? *) +type patches = { + reloc_infos : (reloc_info * int array) array; +} let patch_char4 buff pos c1 c2 c3 c4 = Bytes.unsafe_set buff pos c1; @@ -29,40 +62,48 @@ let patch_char4 buff pos c1 c2 c3 c4 = Bytes.unsafe_set buff (pos + 2) c3; Bytes.unsafe_set buff (pos + 3) c4 -let patch buff (pos, n) = +let patch1 buff pos n = patch_char4 buff pos (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8)) (Char.unsafe_chr (n asr 16)) (Char.unsafe_chr (n asr 24)) -(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *) -let patch_int buff patches = +let patch_int buff reloc = (* copy code *before* patching because of nested evaluations: the code we are patching might be called (and thus "concurrently" patched) and results in wrong results. Side-effects... *) let buff = Bytes.of_string buff in - let () = List.iter (fun p -> patch buff p) patches in - (* Note: we follow the apporach suggested by Gabriel Scherer in - PR#136 here, and use unsafe as we own buff. + let iter (reloc, npos) = Array.iter (fun pos -> patch1 buff pos reloc) npos in + let () = CArray.iter iter reloc in + buff - The crux of the question that avoids defining emitcodes just as a - Byte.t is the call to hcons in to_memory below. Even if disabling - this optimization has no visible time impact, test data shows - that the optimization is indeed triggered quite often so we - choose ugliness over altering the semantics. - - Handle with care. - *) - Bytes.unsafe_to_string buff +let patch buff pl f = + (** Order seems important here? *) + let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in + let buff = patch_int buff reloc in + tcode_of_code buff (Bytes.length buff) (* Buffering of bytecode *) -let out_buffer = ref(Bytes.create 1024) -and out_position = ref 0 +type label_definition = + Label_defined of int + | Label_undefined of (int * int) list -let out_word b1 b2 b3 b4 = - let p = !out_position in - if p >= Bytes.length !out_buffer then begin - let len = Bytes.length !out_buffer in +type env = { + mutable out_buffer : Bytes.t; + mutable out_position : int; + mutable label_table : label_definition array; + (* le ieme element de la table = Label_defined n signifie que l'on a + deja rencontrer le label i et qu'il est a l'offset n. + = Label_undefined l signifie que l'on a + pas encore rencontrer ce label, le premier entier indique ou est l'entier + a patcher dans la string, le deuxieme son origine *) + reloc_info : int list RelocTable.t; +} + +let out_word env b1 b2 b3 b4 = + let p = env.out_position in + if p >= Bytes.length env.out_buffer then begin + let len = Bytes.length env.out_buffer in let new_len = if len <= Sys.max_string_length / 2 then 2 * len @@ -71,260 +112,240 @@ let out_word b1 b2 b3 b4 = then invalid_arg "String.create" (* Pas la bonne exception .... *) else Sys.max_string_length in let new_buffer = Bytes.create new_len in - Bytes.blit !out_buffer 0 new_buffer 0 len; - out_buffer := new_buffer + Bytes.blit env.out_buffer 0 new_buffer 0 len; + env.out_buffer <- new_buffer end; - patch_char4 !out_buffer p (Char.unsafe_chr b1) + patch_char4 env.out_buffer p (Char.unsafe_chr b1) (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4); - out_position := p + 4 + env.out_position <- p + 4 -let out opcode = - out_word opcode 0 0 0 +let out env opcode = + out_word env opcode 0 0 0 -let out_int n = - out_word n (n asr 8) (n asr 16) (n asr 24) +let out_int env n = + out_word env n (n asr 8) (n asr 16) (n asr 24) (* Handling of local labels and backpatching *) -type label_definition = - Label_defined of int - | Label_undefined of (int * int) list - -let label_table = ref ([| |] : label_definition array) -(* le ieme element de la table = Label_defined n signifie que l'on a - deja rencontrer le label i et qu'il est a l'offset n. - = Label_undefined l signifie que l'on a - pas encore rencontrer ce label, le premier entier indique ou est l'entier - a patcher dans la string, le deuxieme son origine *) - -let extend_label_table needed = - let new_size = ref(Array.length !label_table) in +let extend_label_table env needed = + let new_size = ref(Array.length env.label_table) in while needed >= !new_size do new_size := 2 * !new_size done; let new_table = Array.make !new_size (Label_undefined []) in - Array.blit !label_table 0 new_table 0 (Array.length !label_table); - label_table := new_table - -let backpatch (pos, orig) = - let displ = (!out_position - orig) asr 2 in - Bytes.set !out_buffer pos @@ Char.unsafe_chr displ; - Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8); - Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16); - Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24) - -let define_label lbl = - if lbl >= Array.length !label_table then extend_label_table lbl; - match (!label_table).(lbl) with + Array.blit env.label_table 0 new_table 0 (Array.length env.label_table); + env.label_table <- new_table + +let backpatch env (pos, orig) = + let displ = (env.out_position - orig) asr 2 in + Bytes.set env.out_buffer pos @@ Char.unsafe_chr displ; + Bytes.set env.out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8); + Bytes.set env.out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16); + Bytes.set env.out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24) + +let define_label env lbl = + if lbl >= Array.length env.label_table then extend_label_table env lbl; + match (env.label_table).(lbl) with Label_defined _ -> raise(Failure "CEmitcode.define_label") | Label_undefined patchlist -> - List.iter backpatch patchlist; - (!label_table).(lbl) <- Label_defined !out_position + List.iter (fun p -> backpatch env p) patchlist; + (env.label_table).(lbl) <- Label_defined env.out_position -let out_label_with_orig orig lbl = - if lbl >= Array.length !label_table then extend_label_table lbl; - match (!label_table).(lbl) with +let out_label_with_orig env orig lbl = + if lbl >= Array.length env.label_table then extend_label_table env lbl; + match (env.label_table).(lbl) with Label_defined def -> - out_int((def - orig) asr 2) + out_int env ((def - orig) asr 2) | Label_undefined patchlist -> (* spiwack: patchlist is supposed to be non-empty all the time thus I commented that out. If there is no problem I suggest removing it for next release (cur: 8.1) *) (*if patchlist = [] then *) - (!label_table).(lbl) <- - Label_undefined((!out_position, orig) :: patchlist); - out_int 0 + (env.label_table).(lbl) <- + Label_undefined((env.out_position, orig) :: patchlist); + out_int env 0 -let out_label l = out_label_with_orig !out_position l +let out_label env l = out_label_with_orig env env.out_position l (* Relocation information *) -let reloc_info = ref ([] : (reloc_info * int) list) +let enter env info = + let pos = env.out_position in + let old = try RelocTable.find env.reloc_info info with Not_found -> [] in + RelocTable.replace env.reloc_info info (pos :: old) -let enter info = - reloc_info := (info, !out_position) :: !reloc_info +let slot_for_const env c = + enter env (Reloc_const c); + out_int env 0 -let slot_for_const c = - enter (Reloc_const c); - out_int 0 +let slot_for_annot env a = + enter env (Reloc_annot a); + out_int env 0 -let slot_for_annot a = - enter (Reloc_annot a); - out_int 0 - -let slot_for_getglobal p = - enter (Reloc_getglobal p); - out_int 0 +let slot_for_getglobal env p = + enter env (Reloc_getglobal p); + out_int env 0 (* Emission of one instruction *) -let emit_instr = function - | Klabel lbl -> define_label lbl +let emit_instr env = function + | Klabel lbl -> define_label env lbl | Kacc n -> - if n < 8 then out(opACC0 + n) else (out opACC; out_int n) + if n < 8 then out env(opACC0 + n) else (out env opACC; out_int env n) | Kenvacc n -> if n >= 1 && n <= 4 - then out(opENVACC1 + n - 1) - else (out opENVACC; out_int n) + then out env(opENVACC1 + n - 1) + else (out env opENVACC; out_int env n) | Koffsetclosure ofs -> if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2 - then out (opOFFSETCLOSURE0 + ofs / 2) - else (out opOFFSETCLOSURE; out_int ofs) + then out env (opOFFSETCLOSURE0 + ofs / 2) + else (out env opOFFSETCLOSURE; out_int env ofs) | Kpush -> - out opPUSH + out env opPUSH | Kpop n -> - out opPOP; out_int n + out env opPOP; out_int env n | Kpush_retaddr lbl -> - out opPUSH_RETADDR; out_label lbl + out env opPUSH_RETADDR; out_label env lbl | Kapply n -> - if n < 4 then out(opAPPLY1 + n - 1) else (out opAPPLY; out_int n) + if n < 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n) | Kappterm(n, sz) -> - if n < 4 then (out(opAPPTERM1 + n - 1); out_int sz) - else (out opAPPTERM; out_int n; out_int sz) + if n < 4 then (out env(opAPPTERM1 + n - 1); out_int env sz) + else (out env opAPPTERM; out_int env n; out_int env sz) | Kreturn n -> - out opRETURN; out_int n + out env opRETURN; out_int env n | Kjump -> - out opRETURN; out_int 0 + out env opRETURN; out_int env 0 | Krestart -> - out opRESTART + out env opRESTART | Kgrab n -> - out opGRAB; out_int n + out env opGRAB; out_int env n | Kgrabrec(rec_arg) -> - out opGRABREC; out_int rec_arg + out env opGRABREC; out_int env rec_arg | Kclosure(lbl, n) -> - out opCLOSURE; out_int n; out_label lbl + out env opCLOSURE; out_int env n; out_label env lbl | Kclosurerec(nfv,init,lbl_types,lbl_bodies) -> - out opCLOSUREREC;out_int (Array.length lbl_bodies); - out_int nfv; out_int init; - let org = !out_position in - Array.iter (out_label_with_orig org) lbl_types; - let org = !out_position in - Array.iter (out_label_with_orig org) lbl_bodies + out env opCLOSUREREC;out_int env (Array.length lbl_bodies); + out_int env nfv; out_int env init; + let org = env.out_position in + Array.iter (out_label_with_orig env org) lbl_types; + let org = env.out_position in + Array.iter (out_label_with_orig env org) lbl_bodies | Kclosurecofix(nfv,init,lbl_types,lbl_bodies) -> - out opCLOSURECOFIX;out_int (Array.length lbl_bodies); - out_int nfv; out_int init; - let org = !out_position in - Array.iter (out_label_with_orig org) lbl_types; - let org = !out_position in - Array.iter (out_label_with_orig org) lbl_bodies + out env opCLOSURECOFIX;out_int env (Array.length lbl_bodies); + out_int env nfv; out_int env init; + let org = env.out_position in + Array.iter (out_label_with_orig env org) lbl_types; + let org = env.out_position in + Array.iter (out_label_with_orig env org) lbl_bodies | Kgetglobal q -> - out opGETGLOBAL; slot_for_getglobal q + out env opGETGLOBAL; slot_for_getglobal env q | Kconst (Const_b0 i) -> if i >= 0 && i <= 3 - then out (opCONST0 + i) - else (out opCONSTINT; out_int i) + then out env (opCONST0 + i) + else (out env opCONSTINT; out_int env i) | Kconst c -> - out opGETGLOBAL; slot_for_const c + out env opGETGLOBAL; slot_for_const env c | Kmakeblock(n, t) -> if Int.equal n 0 then invalid_arg "emit_instr : block size = 0" - else if n < 4 then (out(opMAKEBLOCK1 + n - 1); out_int t) - else (out opMAKEBLOCK; out_int n; out_int t) + else if n < 4 then (out env(opMAKEBLOCK1 + n - 1); out_int env t) + else (out env opMAKEBLOCK; out_int env n; out_int env t) | Kmakeprod -> - out opMAKEPROD + out env opMAKEPROD | Kmakeswitchblock(typlbl,swlbl,annot,sz) -> - out opMAKESWITCHBLOCK; - out_label typlbl; out_label swlbl; - slot_for_annot annot;out_int sz + out env opMAKESWITCHBLOCK; + out_label env typlbl; out_label env swlbl; + slot_for_annot env annot;out_int env sz | Kswitch (tbl_const, tbl_block) -> let lenb = Array.length tbl_block in let lenc = Array.length tbl_const in assert (lenb < 0x100 && lenc < 0x1000000); - out opSWITCH; - out_word lenc (lenc asr 8) (lenc asr 16) (lenb); -(* out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); *) - let org = !out_position in - Array.iter (out_label_with_orig org) tbl_const; - Array.iter (out_label_with_orig org) tbl_block + out env opSWITCH; + out_word env lenc (lenc asr 8) (lenc asr 16) (lenb); +(* out_int env (Array.length tbl_const + (Array.length tbl_block lsl 23)); *) + let org = env.out_position in + Array.iter (out_label_with_orig env org) tbl_const; + Array.iter (out_label_with_orig env org) tbl_block | Kpushfields n -> - out opPUSHFIELDS;out_int n + out env opPUSHFIELDS;out_int env n | Kfield n -> - if n <= 1 then out (opGETFIELD0+n) - else (out opGETFIELD;out_int n) + if n <= 1 then out env (opGETFIELD0+n) + else (out env opGETFIELD;out_int env n) | Ksetfield n -> - if n <= 1 then out (opSETFIELD0+n) - else (out opSETFIELD;out_int n) + if n <= 1 then out env (opSETFIELD0+n) + else (out env opSETFIELD;out_int env n) | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr" - | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p) - | Kensurestackcapacity size -> out opENSURESTACKCAPACITY; out_int size + | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_const env (Const_proj p) + | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size (* spiwack *) - | Kbranch lbl -> out opBRANCH; out_label lbl - | Kaddint31 -> out opADDINT31 - | Kaddcint31 -> out opADDCINT31 - | Kaddcarrycint31 -> out opADDCARRYCINT31 - | Ksubint31 -> out opSUBINT31 - | Ksubcint31 -> out opSUBCINT31 - | Ksubcarrycint31 -> out opSUBCARRYCINT31 - | Kmulint31 -> out opMULINT31 - | Kmulcint31 -> out opMULCINT31 - | Kdiv21int31 -> out opDIV21INT31 - | Kdivint31 -> out opDIVINT31 - | Kaddmuldivint31 -> out opADDMULDIVINT31 - | Kcompareint31 -> out opCOMPAREINT31 - | Khead0int31 -> out opHEAD0INT31 - | Ktail0int31 -> out opTAIL0INT31 - | Kisconst lbl -> out opISCONST; out_label lbl - | Kareconst(n,lbl) -> out opARECONST; out_int n; out_label lbl - | Kcompint31 -> out opCOMPINT31 - | Kdecompint31 -> out opDECOMPINT31 - | Klorint31 -> out opORINT31 - | Klandint31 -> out opANDINT31 - | Klxorint31 -> out opXORINT31 + | Kbranch lbl -> out env opBRANCH; out_label env lbl + | Kaddint31 -> out env opADDINT31 + | Kaddcint31 -> out env opADDCINT31 + | Kaddcarrycint31 -> out env opADDCARRYCINT31 + | Ksubint31 -> out env opSUBINT31 + | Ksubcint31 -> out env opSUBCINT31 + | Ksubcarrycint31 -> out env opSUBCARRYCINT31 + | Kmulint31 -> out env opMULINT31 + | Kmulcint31 -> out env opMULCINT31 + | Kdiv21int31 -> out env opDIV21INT31 + | Kdivint31 -> out env opDIVINT31 + | Kaddmuldivint31 -> out env opADDMULDIVINT31 + | Kcompareint31 -> out env opCOMPAREINT31 + | Khead0int31 -> out env opHEAD0INT31 + | Ktail0int31 -> out env opTAIL0INT31 + | Kisconst lbl -> out env opISCONST; out_label env lbl + | Kareconst(n,lbl) -> out env opARECONST; out_int env n; out_label env lbl + | Kcompint31 -> out env opCOMPINT31 + | Kdecompint31 -> out env opDECOMPINT31 + | Klorint31 -> out env opORINT31 + | Klandint31 -> out env opANDINT31 + | Klxorint31 -> out env opXORINT31 (*/spiwack *) | Kstop -> - out opSTOP + out env opSTOP (* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *) -let rec emit insns remaining = match insns with +let rec emit env insns remaining = match insns with | [] -> (match remaining with [] -> () - | (first::rest) -> emit first rest) + | (first::rest) -> emit env first rest) (* Peephole optimizations *) | Kpush :: Kacc n :: c -> - if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n); - emit c remaining + if n < 8 then out env(opPUSHACC0 + n) else (out env opPUSHACC; out_int env n); + emit env c remaining | Kpush :: Kenvacc n :: c -> if n >= 1 && n <= 4 - then out(opPUSHENVACC1 + n - 1) - else (out opPUSHENVACC; out_int n); - emit c remaining + then out env(opPUSHENVACC1 + n - 1) + else (out env opPUSHENVACC; out_int env n); + emit env c remaining | Kpush :: Koffsetclosure ofs :: c -> if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2 - then out(opPUSHOFFSETCLOSURE0 + ofs / 2) - else (out opPUSHOFFSETCLOSURE; out_int ofs); - emit c remaining + then out env(opPUSHOFFSETCLOSURE0 + ofs / 2) + else (out env opPUSHOFFSETCLOSURE; out_int env ofs); + emit env c remaining | Kpush :: Kgetglobal id :: c -> - out opPUSHGETGLOBAL; slot_for_getglobal id; emit c remaining + out env opPUSHGETGLOBAL; slot_for_getglobal env id; emit env c remaining | Kpush :: Kconst (Const_b0 i) :: c -> if i >= 0 && i <= 3 - then out (opPUSHCONST0 + i) - else (out opPUSHCONSTINT; out_int i); - emit c remaining + then out env (opPUSHCONST0 + i) + else (out env opPUSHCONSTINT; out_int env i); + emit env c remaining | Kpush :: Kconst const :: c -> - out opPUSHGETGLOBAL; slot_for_const const; - emit c remaining + out env opPUSHGETGLOBAL; slot_for_const env const; + emit env c remaining | Kpop n :: Kjump :: c -> - out opRETURN; out_int n; emit c remaining + out env opRETURN; out_int env n; emit env c remaining | Ksequence(c1,c2)::c -> - emit c1 (c2::c::remaining) + emit env c1 (c2::c::remaining) (* Default case *) | instr :: c -> - emit_instr instr; emit c remaining + emit_instr env instr; emit env c remaining (* Initialization *) -let init () = - out_position := 0; - label_table := Array.make 16 (Label_undefined []); - reloc_info := [] - -type emitcodes = String.t - -let length = String.length - -type to_patch = emitcodes * (patch list) * fv +type to_patch = emitcodes * patches * fv (* Substitution *) let rec subst_strcst s sc = @@ -334,17 +355,21 @@ let rec subst_strcst s sc = | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) -let subst_patch s (ri,pos) = +let subst_reloc s ri = match ri with | Reloc_annot a -> let (kn,i) = a.ci.ci_ind in let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in - (Reloc_annot {a with ci = ci},pos) - | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) - | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos) + Reloc_annot {a with ci = ci} + | Reloc_const sc -> Reloc_const (subst_strcst s sc) + | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn) + +let subst_patches subst p = + let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in + { reloc_infos = infos; } let subst_to_patch s (code,pl,fv) = - code,List.rev_map (subst_patch s) pl,fv + code, subst_patches s pl, fv type body_code = | BCdefined of to_patch @@ -381,16 +406,23 @@ let repr_body_code = function | PBCconstant -> (None, BCconstant) let to_memory (init_code, fun_code, fv) = - init(); - emit init_code []; - emit fun_code []; + let env = { + out_buffer = Bytes.create 1024; + out_position = 0; + label_table = Array.make 16 (Label_undefined []); + reloc_info = RelocTable.create 91; + } in + emit env init_code []; + emit env fun_code []; (** Later uses of this string are all purely functional *) - let code = Bytes.sub_string !out_buffer 0 !out_position in + let code = Bytes.sub_string env.out_buffer 0 env.out_position in let code = CString.hcons code in - let reloc = List.rev !reloc_info in + let fold reloc npos accu = (reloc, Array.of_list npos) :: accu in + let reloc = RelocTable.fold fold env.reloc_info [] in + let reloc = { reloc_infos = CArray.of_list reloc } in Array.iter (fun lbl -> (match lbl with Label_defined _ -> assert true | Label_undefined patchlist -> - assert (patchlist = []))) !label_table; + assert (patchlist = []))) env.label_table; (code, reloc, fv) diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index fee45aafd..03920dc1a 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -6,20 +6,12 @@ type reloc_info = | Reloc_const of structured_constant | Reloc_getglobal of Constant.t -type patch = reloc_info * int - -(* A virer *) -val subst_patch : Mod_subst.substitution -> patch -> patch - +type patches type emitcodes -val length : emitcodes -> int - -val patch_int : emitcodes -> ((*pos*)int * int) list -> emitcodes - -type to_patch = emitcodes * (patch list) * fv +val patch : emitcodes -> patches -> (reloc_info -> int) -> Vmvalues.tcode -val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch +type to_patch = emitcodes * patches * fv type body_code = | BCdefined of to_patch diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 2bbb867cd..55430a9d8 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -14,7 +14,6 @@ open Util open Names -open Constr open Vmvalues open Cemitcodes open Cbytecodes @@ -25,7 +24,6 @@ open Cbytegen module NamedDecl = Context.Named.Declaration module RelDecl = Context.Rel.Declaration -external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code" external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" (*******************) @@ -56,61 +54,12 @@ let set_global v = (* table pour les structured_constant et les annotations des switchs *) -let rec eq_structured_constant c1 c2 = match c1, c2 with -| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 -| Const_sorts _, _ -> false -| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 -| Const_ind _, _ -> false -| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 -| Const_proj _, _ -> false -| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 -| Const_b0 _, _ -> false -| Const_bn (t1, a1), Const_bn (t2, a2) -> - Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2 -| Const_bn _, _ -> false -| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 -| Const_univ_level _ , _ -> false -| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 -| Const_type _ , _ -> false - -let rec hash_structured_constant c = - let open Hashset.Combine in - match c with - | Const_sorts s -> combinesmall 1 (Sorts.hash s) - | Const_ind i -> combinesmall 2 (ind_hash i) - | Const_proj p -> combinesmall 3 (Constant.hash p) - | Const_b0 t -> combinesmall 4 (Int.hash t) - | Const_bn (t, a) -> - let fold h c = combine h (hash_structured_constant c) in - let h = Array.fold_left fold 0 a in - combinesmall 5 (combine (Int.hash t) h) - | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) - | Const_type u -> combinesmall 7 (Univ.Universe.hash u) - module SConstTable = Hashtbl.Make (struct type t = structured_constant let equal = eq_structured_constant let hash = hash_structured_constant end) -let eq_annot_switch asw1 asw2 = - let eq_ci ci1 ci2 = - eq_ind ci1.ci_ind ci2.ci_ind && - Int.equal ci1.ci_npar ci2.ci_npar && - Array.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls - in - let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in - eq_ci asw1.ci asw2.ci && - Array.equal eq_rlc asw1.rtbl asw2.rtbl && - (asw1.tailcall : bool) == asw2.tailcall - -let hash_annot_switch asw = - let open Hashset.Combine in - let h1 = Constr.case_info_hash asw.ci in - let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in - let h3 = if asw.tailcall then 1 else 0 in - combine3 h1 h2 h3 - module AnnotTable = Hashtbl.Make (struct type t = annot_switch let equal = eq_annot_switch @@ -205,15 +154,13 @@ and slot_for_fv env fv = assert false and eval_to_patch env (buff,pl,fv) = - let patch = function - | Reloc_annot a, pos -> (pos, slot_for_annot a) - | Reloc_const sc, pos -> (pos, slot_for_str_cst sc) - | Reloc_getglobal kn, pos -> (pos, slot_for_getglobal env kn) + let slots = function + | Reloc_annot a -> slot_for_annot a + | Reloc_const sc -> slot_for_str_cst sc + | Reloc_getglobal kn -> slot_for_getglobal env kn in - let patches = List.map_left patch pl in - let buff = patch_int buff patches in + let tc = patch buff pl slots in let vm_env = Array.map (slot_for_fv env) fv in - let tc = tcode_of_code buff (length buff) in eval_tcode tc vm_env and val_of_constr env c = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 159d2ea66..da7042713 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -882,6 +882,18 @@ let hnf_prod_app env t n = let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl +let hnf_prod_applist_assum env n c l = + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Too many arguments.") + else match kind (whd_allnolet env t), l with + | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") + | _ -> anomaly (Pp.str "Not enough prod/let's.") in + app n [] c l + (* Dealing with arities *) let dest_prod env = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 0e6a2b819..6f7e3f8f8 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -105,6 +105,12 @@ val beta_app : constr -> constr -> constr (** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types +(** In [hnf_prod_applist_assum n c args], [c] is supposed to (whd-)reduce to + the form [∀Γ.t] with [Γ] of length [n] and possibly with let-ins; it + returns [t] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val hnf_prod_applist_assum : env -> int -> types -> constr list -> types + (** Compatibility alias for Term.lambda_appvect_assum *) val betazeta_appvect : int -> constr -> constr array -> constr diff --git a/kernel/term.ml b/kernel/term.ml index fae990d45..a4c92bd33 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -352,10 +352,11 @@ let lambda_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments.") + else anomaly (Pp.str "Too many arguments.") else match kind_of_term t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l @@ -377,10 +378,11 @@ let prod_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments.") + else anomaly (Pp.str "Too many arguments.") else match kind_of_term t, l with | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") | _ -> anomaly (Pp.str "Not enough prod/let's.") in app n [] c l diff --git a/kernel/term.mli b/kernel/term.mli index c9a8cf6e1..b4597676a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -242,7 +242,7 @@ val lambda_applist : constr -> constr list -> constr val lambda_appvect : constr -> constr array -> constr (** In [lambda_applist_assum n c args], [c] is supposed to have the - form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it + form [λΓ.c] with [Γ] of length [n] and possibly with let-ins; it returns [c] with the assumptions of [Γ] instantiated by [args] and the local definitions of [Γ] expanded. *) val lambda_applist_assum : int -> constr -> constr list -> constr @@ -251,15 +251,15 @@ val lambda_appvect_assum : int -> constr -> constr array -> constr (** pseudo-reduction rule *) (** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *) -val prod_appvect : constr -> constr array -> constr -val prod_applist : constr -> constr list -> constr +val prod_appvect : types -> constr array -> types +val prod_applist : types -> constr list -> types (** In [prod_appvect_assum n c args], [c] is supposed to have the - form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it + form [∀Γ.c] with [Γ] of length [n] and possibly with let-ins; it returns [c] with the assumptions of [Γ] instantiated by [args] and the local definitions of [Γ] expanded. *) -val prod_appvect_assum : int -> constr -> constr array -> constr -val prod_applist_assum : int -> constr -> constr list -> constr +val prod_appvect_assum : int -> types -> constr array -> types +val prod_applist_assum : int -> types -> constr list -> types (** {5 Other term destructors. } *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5f501bff1..9b864440d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -223,9 +223,8 @@ let rec unzip ctx j = unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } let feedback_completion_typecheck = - let open Feedback in Option.iter (fun state_id -> - feedback ~id:state_id Feedback.Complete) + Feedback.feedback ~id:state_id Feedback.Complete) let abstract_constant_universes = function | Monomorphic_const_entry uctx -> diff --git a/kernel/univ.ml b/kernel/univ.ml index 080bb7ad4..fbb047364 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -266,7 +266,7 @@ struct module Expr = struct type t = Level.t * int - + (* Hashing of expressions *) module ExprHash = struct @@ -487,7 +487,40 @@ struct | [] -> cons a l in List.fold_right (fun a acc -> aux a acc) u [] - + + (** [max_var_pred p u] returns the maximum variable level in [u] satisfying + [p], -1 if not found *) + let rec max_var_pred p u = + let open Level in + match u with + | [] -> -1 + | (v, _) :: u -> + match var_index v with + | Some i when p i -> max i (max_var_pred p u) + | _ -> max_var_pred p u + + let rec remap_var u i j = + let open Level in + match u with + | [] -> [] + | (v, incr) :: u when var_index v = Some i -> + (Level.var j, incr) :: remap_var u i j + | _ :: u -> remap_var u i j + + let rec compact u max_var i = + if i >= max_var then (u,[]) else + let j = max_var_pred (fun j -> j < i) u in + if Int.equal i (j+1) then + let (u,s) = compact u max_var (i+1) in + (u, i :: s) + else + let (u,s) = compact (remap_var u i j) max_var (i+1) in + (u, j+1 :: s) + + let compact u = + let max_var = max_var_pred (fun _ -> true) u in + compact u max_var 0 + (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) let sup x y = merge_univs x y diff --git a/kernel/univ.mli b/kernel/univ.mli index 77ebf5a11..c45ebe21c 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -125,6 +125,13 @@ sig val for_all : (Level.t * int -> bool) -> t -> bool val map : (Level.t * int -> 'a) -> t -> 'a list + + (** [compact u] remaps local variables in [u] such that their indices become + consecutive. It returns the new universe and the mapping. + Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] = + [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2] + *) + val compact : t -> t * int list end type universe = Universe.t diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 1102cdec1..2d8a1d976 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -8,6 +8,7 @@ open Names open Sorts open Cbytecodes +open Univ (*******************************************) (* Initalization of the abstract machine ***) @@ -189,11 +190,11 @@ let rec whd_accu a stk = | i when Int.equal i type_atom_tag -> begin match stk with | [Zapp args] -> - let u = ref (Obj.obj (Obj.field at 0)) in - for i = 0 to nargs args - 1 do - u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) - done; - Vsort (Type !u) + let args = Array.init (nargs args) (arg args) in + let u = Obj.obj (Obj.field at 0) in + let inst = Instance.of_array (Array.map uni_lvl_val args) in + let u = Univ.subst_instance_universe inst u in + Vsort (Type u) | _ -> assert false end | i when i <= max_atom_tag -> diff --git a/lib/envars.ml b/lib/envars.ml index 8ebf84057..9b66c1f71 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -155,23 +155,21 @@ let exe s = s ^ Coq_config.exec_extension let ocamlfind () = Coq_config.ocamlfind -(** {2 Camlp4 paths} *) +(** {2 Camlp5 paths} *) -let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4) +let guess_camlp5bin () = which (user_path ()) (exe "camlp5") -let camlp4bin () = - if !Flags.boot then Coq_config.camlp4bin else - try guess_camlp4bin () +let camlp5bin () = + if !Flags.boot then Coq_config.camlp5bin else + try guess_camlp5bin () with Not_found -> - Coq_config.camlp4bin + Coq_config.camlp5bin -let camlp4 () = camlp4bin () / exe Coq_config.camlp4 - -let camlp4lib () = +let camlp5lib () = if !Flags.boot then - Coq_config.camlp4lib + Coq_config.camlp5lib else - let ex, res = CUnix.run_command (ocamlfind () ^ " query " ^ Coq_config.camlp4) in + let ex, res = CUnix.run_command (ocamlfind () ^ " query camlp5") in match ex with | Unix.WEXITED 0 -> String.strip res | _ -> "/dev/null" @@ -206,11 +204,10 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); - fprintf f "%sCAMLP4=%s\n" prefix_var_name Coq_config.camlp4; - fprintf f "%sCAMLP4O=%s\n" prefix_var_name Coq_config.camlp4o; - fprintf f "%sCAMLP4BIN=%s/\n" prefix_var_name (camlp4bin ()); - fprintf f "%sCAMLP4LIB=%s\n" prefix_var_name (camlp4lib ()); - fprintf f "%sCAMLP4OPTIONS=%s\n" prefix_var_name Coq_config.camlp4compat; + fprintf f "%sCAMLP5O=%s\n" prefix_var_name Coq_config.camlp5o; + fprintf f "%sCAMLP5BIN=%s/\n" prefix_var_name (camlp5bin ()); + fprintf f "%sCAMLP5LIB=%s\n" prefix_var_name (camlp5lib ()); + fprintf f "%sCAMLP5OPTIONS=%s\n" prefix_var_name Coq_config.camlp5compat; fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); diff --git a/lib/envars.mli b/lib/envars.mli index 09f2b4ca1..1ccd1feff 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -56,14 +56,11 @@ val coqpath : string list (** [camlfind ()] is the path to the ocamlfind binary. *) val ocamlfind : unit -> string -(** [camlp4bin ()] is the path to the camlp4 binary. *) -val camlp4bin : unit -> string +(** [camlp5bin ()] is the path to the camlp5 binary. *) +val camlp5bin : unit -> string -(** [camlp4lib ()] is the path to the camlp4 library. *) -val camlp4lib : unit -> string - -(** [camlp4 ()] is the camlp4 utility. *) -val camlp4 : unit -> string +(** [camlp5lib ()] is the path to the camlp5 library. *) +val camlp5lib : unit -> string (** Coq tries to honor the XDG Base Directory Specification to access the user's configuration files. diff --git a/lib/flags.ml b/lib/flags.ml index 01361dad5..415e4399a 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -56,10 +56,8 @@ let in_toplevel = ref false let profile = false let ide_slave = ref false -let ideslave_coqtop_flags = ref None let raw_print = ref false - let univ_print = ref false let we_are_parsing = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 33d281798..c82410f07 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -33,7 +33,6 @@ val profile : bool (* -ide_slave: printing will be more verbose, will affect stm caching *) val ide_slave : bool ref -val ideslave_coqtop_flags : string option ref (* development flag to detect race conditions, it should go away. *) val we_are_parsing : bool ref diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 9c2766187..ea6266dd4 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -21,11 +21,11 @@ open Names a reference to the current level (to be translated into "SELF" on the left border and into "constr LEVEL n" elsewhere), to the level below (to be translated into "NEXT") or to an below wrt associativity (to be - translated in camlp4 into "constr" without level) or to another level + translated in camlp5 into "constr" without level) or to another level (to be translated into "constr LEVEL n") The boolean is true if the entry was existing _and_ empty; this to - circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the + circumvent a weakness of camlp5 whose undo mechanism is not the converse of the extension mechanism *) let constr_level = string_of_int @@ -144,11 +144,11 @@ let find_position accu forpat assoc level = (**************************************************************************) (* - * --- Note on the mapping of grammar productions to camlp4 actions --- + * --- Note on the mapping of grammar productions to camlp5 actions --- * * Translation of environments: a production * [ nt1(x1) ... nti(xi) ] -> act(x1..xi) - * is written (with camlp4 conventions): + * is written (with camlp5 conventions): * (fun vi -> .... (fun v1 -> act(v1 .. vi) )..) * where v1..vi are the values generated by non-terminals nt1..nti. * Since the actions are executed by substituting an environment, @@ -172,8 +172,8 @@ let find_position accu forpat assoc level = (**********************************************************************) (* Binding constr entry keys to entries *) -(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) -let camlp4_assoc = function +(* Camlp5 levels do not treat NonA: use RightA with a NEXT on the left *) +let camlp5_assoc = function | Some NonA | Some RightA -> RightA | None | Some LeftA -> LeftA @@ -205,7 +205,7 @@ let adjust_level assoc from = function (* If NonA on the left-hand side, adopt the current assoc ?? *) | (NumLevel n,BorderProd (Left,Some NonA)) -> None (* If the expected assoc is the current one, set to SELF *) - | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) -> + | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) -> None (* Otherwise, force the level, n or n-1, according to expected assoc *) | (NumLevel n,BorderProd (Left,Some a)) -> diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 8e0469275..1e3869818 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Mapping of grammar productions to camlp4 actions *) +(** Mapping of grammar productions to camlp5 actions *) (** This is the part specific to Coq-level Notation and Tactic Notation. For the ML-level tactic and vernac extensions, see Egramml. *) diff --git a/parsing/egramml.mli b/parsing/egramml.mli index 7414773d3..74dd95a20 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -8,7 +8,7 @@ open Vernacexpr -(** Mapping of grammar productions to camlp4 actions. *) +(** Mapping of grammar productions to camlp5 actions. *) (** This is the part specific to vernac extensions. For the Coq-level Notation and Tactic Notation, see Egramcoq. *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3244b0ff2..d42b5f622 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -17,7 +17,7 @@ open Vernacexpr open Decl_kinds open Declarations open Misctypes -open Tok (* necessary for camlp4 *) +open Tok (* necessary for camlp5 *) open Pcoq open Pcoq.Prim @@ -827,7 +827,7 @@ GEXTEND Gram command: [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l - (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) + (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; info = hint_info -> diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index c934d38a2..54e7949ae 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -202,7 +202,7 @@ end = struct end -let camlp4_verbosity silent f x = +let camlp5_verbosity silent f x = let a = !warning_verbose in warning_verbose := silent; f x; @@ -274,7 +274,7 @@ type ext_kind = (** The list of extensions *) -let camlp4_state = ref [] +let camlp5_state = ref [] (** Deletion *) @@ -299,13 +299,13 @@ let grammar_delete e reinit (pos,rls) = let grammar_extend e reinit ext = let ext = of_coq_extend_statement ext in let undo () = grammar_delete e reinit ext in - let redo () = camlp4_verbosity false (uncurry (G.extend e)) ext in - camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state; + let redo () = camlp5_verbosity false (uncurry (G.extend e)) ext in + camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e reinit ext = - camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state; - camlp4_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext) + camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state; + camlp5_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext) (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -315,20 +315,20 @@ module Gram = include G let extend e = curry - (fun ext -> - camlp4_state := - (ByEXTEND ((fun () -> grammar_delete e None ext), - (fun () -> uncurry (G.extend e) ext))) - :: !camlp4_state; - uncurry (G.extend e) ext) + (fun ext -> + camlp5_state := + (ByEXTEND ((fun () -> grammar_delete e None ext), + (fun () -> uncurry (G.extend e) ext))) + :: !camlp5_state; + uncurry (G.extend e) ext) let delete_rule e pil = (* spiwack: if you use load an ML module which contains GDELETE_RULE - in a section, God kills a kitty. As it would corrupt remove_grammars. + in a section, God kills a kitty. As it would corrupt remove_grammars. There does not seem to be a good way to undo a delete rule. As deleting - takes fewer arguments than extending. The production rule isn't returned - by delete_rule. If we could retrieve the necessary information, then - ByEXTEND provides just the framework we need to allow this in section. - I'm not entirely sure it makes sense, but at least it would be more correct. + takes fewer arguments than extending. The production rule isn't returned + by delete_rule. If we could retrieve the necessary information, then + ByEXTEND provides just the framework we need to allow this in section. + I'm not entirely sure it makes sense, but at least it would be more correct. *) G.delete_rule e pil end @@ -340,18 +340,18 @@ module Gram = let rec remove_grammars n = if n>0 then - (match !camlp4_state with + (match !camlp5_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.") | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> grammar_delete g reinit (of_coq_extend_statement ext); - camlp4_state := t; + camlp5_state := t; remove_grammars (n-1) | ByEXTEND (undo,redo)::t -> undo(); - camlp4_state := t; + camlp5_state := t; remove_grammars n; redo(); - camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state) + camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state) let make_rule r = [None, None, r] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 756d9487d..75378d2c6 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -124,7 +124,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e | | Egrammar.make_constr_prod_item V - Gramext.g_symbol list which is sent to camlp4 + Gramext.g_symbol list which is sent to camlp5 For user level tactic notations, dynamic addition of new rules is also done in several steps: @@ -161,9 +161,9 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e *) -(** Temporarily activate camlp4 verbosity *) +(** Temporarily activate camlp5 verbosity *) -val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit +val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit (** Parse a string *) diff --git a/parsing/tok.ml b/parsing/tok.ml index 0917e8d6d..fafad2779 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -60,7 +60,7 @@ let match_keyword kwd = function | KEYWORD kwd' when kwd = kwd' -> true | _ -> false -(* Needed to fix Camlp4 signature. +(* Needed to fix Camlp5 signature. Cannot use Pp because of silly Tox -> Compat -> Pp dependency *) let print ppf tok = Format.pp_print_string ppf (to_string tok) diff --git a/parsing/tok.mli b/parsing/tok.mli index 59a79dcd2..162310e2a 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -22,7 +22,7 @@ type t = val equal : t -> t -> bool val extract_string : t -> string val to_string : t -> string -(* Needed to fit Camlp4 signature *) +(* Needed to fit Camlp5 signature *) val print : Format.formatter -> t -> unit val match_keyword : string -> t -> bool (** for camlp5 *) diff --git a/plugins/.dir-locals.el b/plugins/.dir-locals.el deleted file mode 100644 index 4e8830f6c..000000000 --- a/plugins/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -((coq-mode . ((eval . (let ((default-directory (locate-dominating-file - buffer-file-name ".dir-locals.el"))) - (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq")) - (setq-local coq-prog-name (expand-file-name "../bin/coqtop"))))))) diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4 index 23b91507c..896bb91f1 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin DECLARE PLUGIN "btauto_plugin" diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 6ed4672ce..0d677ac7a 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin open Cctac open Stdarg diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index df701ed80..72057cd9b 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -8,8 +8,6 @@ open Stdarg -(*i camlp4deps: "grammar/grammar.cma" i*) - DECLARE PLUGIN "derive_plugin" let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 24c70bccf..4b6de58bd 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Pcoq.Prim DECLARE PLUGIN "extraction_plugin" diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index b81010c7b..3c6ab47e9 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin open Formula diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index 682673e8d..16dd4c886 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin open FourierR diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 4b828a702..ac7a2f284 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -5,7 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin open Util open Pp diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 2769802cf..7d2c4d082 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Util open Locus open Misctypes diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index bb01aca55..4c6d3c2d3 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Pp open Genarg open Stdarg diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 3e3965b94..286f9d95d 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Pp open Genarg open Stdarg diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 90a44708f..f74d24db0 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Pp open Genarg open Stdarg diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index ed2d9da63..014433ac4 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Class_tactics open Stdarg open Tacarg diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index 549436902..f705778fc 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -12,8 +12,6 @@ (* by Eduardo Gimenez *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Eqdecide DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index cc7ce339b..9ef819569 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - DECLARE PLUGIN "ltac_plugin" open Util @@ -17,7 +15,7 @@ open Tacexpr open Misctypes open Genarg open Genredexpr -open Tok (* necessary for camlp4 *) +open Tok (* necessary for camlp5 *) open Names open Pcoq diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index f6cc3833a..e251b1049 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -6,11 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - (* Syntax for the subtac terms and types. - Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) + Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) open Libnames open Constrexpr diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index ea1808a25..2459a09bc 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - (* Syntax for rewriting with strategies *) open Names diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 9864ffeb6..7a75662be 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - (** Ltac profiling entrypoints *) open Profile_ltac diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index b15dd7ae6..9f1d83f96 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -14,8 +14,6 @@ (* *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin open Stdarg open Tacarg diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 01c3d7940..272d4a20f 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin DECLARE PLUGIN "nsatz_plugin" diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 735af6bab..f7b153a13 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -13,8 +13,6 @@ (* *) (**************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - DECLARE PLUGIN "omega_plugin" diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index f7ebd3204..40897d62f 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin open Names open Misctypes diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 5fd9c9419..5b77d08de 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -6,8 +6,6 @@ *************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - DECLARE PLUGIN "romega_plugin" diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index bfa1e5f39..1bfcdc2fb 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -7,8 +7,6 @@ (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin DECLARE PLUGIN "rtauto_plugin" diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index a7d6d5bb2..b34d12952 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin open Pp open Util diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 5c06cf426..9822da1c7 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -745,7 +745,7 @@ let discharge_hyp (id', (id, mode)) gl = let cl' = Vars.subst_var id (pf_concl gl) in match pf_get_hyp gl id, mode with | NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" -> - Proofview.V82.of_tactic (Tactics.apply_type (EConstr.of_constr (mkProd (Name id', t, cl'))) + Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false (EConstr.of_constr (mkProd (Name id', t, cl'))) [EConstr.of_constr (mkVar id)]) gl | NamedDecl.LocalDef (_, v, t), _ -> Proofview.V82.of_tactic @@ -1179,7 +1179,7 @@ let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) = false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl else CErrors.user_err ?loc:(loc_of_cpattern t) (str "generalized term didn't match") -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs) +let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) let genclrtac cl cs clr = let tclmyORELSE tac1 tac2 gl = diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 4e0b44a44..5782a7621 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -28,7 +28,7 @@ module RelDecl = Context.Rel.Declaration (** The "case" and "elim" tactic *) -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs) +let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) (* TASSI: given the type of an elimination principle, it finds the higher order * argument (index), it computes it's arity and the arity of the eliminator and diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 6032ed2af..11ebe4337 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -382,7 +382,7 @@ let is_construct_ref sigma c r = EConstr.isConstruct sigma c && eq_gr (ConstructRef (fst(EConstr.destConstruct sigma c))) r let is_ind_ref sigma c r = EConstr.isInd sigma c && eq_gr (IndRef (fst(EConstr.destInd sigma c))) r -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs) +let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) let rwcltac cl rdx dir sr gl = let n, r_n,_, ucst = pf_abs_evars gl sr in diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 6c325cce4..b3be31b7b 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -41,7 +41,7 @@ module RelDecl = Context.Rel.Declaration (* They require guessing the view hints and the number of *) (* implicits, respectively, which we do by brute force. *) -let apply_type x xs = Proofview.V82.of_tactic (apply_type x xs) +let apply_type x xs = Proofview.V82.of_tactic (apply_type ~typecheck:false x xs) let new_tac = Proofview.V82.of_tactic diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 5e43c8374..6514b186e 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -122,7 +122,7 @@ let endclausestac id_map clseq gl_id cl0 gl = if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else CErrors.user_err (Pp.str "tampering with discharged assumptions of \"in\" tactical") -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs) +let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) let tclCLAUSES ist tac (gens, clseq) gl = if clseq = InGoal || clseq = InSeqGoal then tac gl else diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index d6dbad7a9..7d0584a00 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -12,9 +12,6 @@ * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; -(*i camlp4use: "pa_extend.cmo" i*) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin open Names open Pp diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 754e88139..18ecbf8ed 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -451,17 +451,15 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = then Anonymous, None, None else - match Option.map detype p with - | None -> Anonymous, None, None - | Some p -> - let nl,typ = it_destRLambda_or_LetIn_names k p in - let n,typ = match DAst.get typ with - | GLambda (x,_,t,c) -> x, c - | _ -> Anonymous, typ in - let aliastyp = - if List.for_all (Name.equal Anonymous) nl then None - else Some (Loc.tag (indsp,nl)) in - n, aliastyp, Some typ + let p = detype p in + let nl,typ = it_destRLambda_or_LetIn_names k p in + let n,typ = match DAst.get typ with + | GLambda (x,_,t,c) -> x, c + | _ -> Anonymous, typ in + let aliastyp = + if List.for_all (Name.equal Anonymous) nl then None + else Some (Loc.tag (indsp,nl)) in + n, aliastyp, Some typ in let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in let tag = @@ -650,7 +648,7 @@ and detype_r d flags avoid env sigma t = (is_nondep_branch sigma) avoid (ci.ci_ind,ci.ci_pp_info.style, ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) - (Some p) c bl + p c bl | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index a0a8276c5..a4097237f 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -159,34 +159,21 @@ and infer_vect infos variances v = let infer_term cv_pb env variances c = let open CClosure in - let reds = RedFlags.red_add_transparent betaiotazeta Names.full_transparent_state in - let infos = create_clos_infos reds env in + let infos = create_clos_infos all env in infer_fterm cv_pb infos variances (CClosure.inject c) [] -let infer_arity_constructor env variances arcn is_arity params = - let numchecked = ref 0 in - let numparams = Context.Rel.nhyps params in - let basic_check env variances tp = - let variances = - if !numchecked >= numparams then - infer_term CUMUL env variances tp - else - variances - in - numchecked := !numchecked + 1; variances - in +let infer_arity_constructor is_arity env variances arcn = let infer_typ typ (env,variances) = match typ with | Context.Rel.Declaration.LocalAssum (_, typ') -> - (Environ.push_rel typ env, basic_check env variances typ') + (Environ.push_rel typ env, infer_term CUMUL env variances typ') | Context.Rel.Declaration.LocalDef _ -> assert false in - let arcn' = Term.it_mkProd_or_LetIn arcn params in - let typs, codom = Reduction.dest_prod env arcn' in + let typs, codom = Reduction.dest_prod env arcn in let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j} i is irrelevant, j is invariant. *) - if not is_arity then basic_check env variances codom else variances + if not is_arity then infer_term CUMUL env variances codom else variances let infer_inductive env mie = let open Entries in @@ -205,15 +192,12 @@ let infer_inductive env mie = Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) LMap.empty uarray in + let env, _ = Typeops.infer_local_decls env params in let variances = List.fold_left (fun variances entry -> - let _, params = Typeops.infer_local_decls env params in - let variances = infer_arity_constructor - env variances entry.mind_entry_arity true params + let variances = infer_arity_constructor true + env variances entry.mind_entry_arity in - List.fold_left - (fun variances cons -> - infer_arity_constructor - env variances cons false params) + List.fold_left (infer_arity_constructor false env) variances entry.mind_entry_lc) variances entries diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b21fbf0eb..c93b41786 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -240,8 +240,9 @@ and nf_stk ?from:(from=0) env sigma c t stk = let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in + let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = - hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in + hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in let pT = whd_all env pT in let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 35487e09c..2cdb9be3f 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -93,10 +93,11 @@ let print_one_inductive env sigma mib ((_,i) as ind) = else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in + let nparamdecls = Context.Rel.length params in let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in - let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in + let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in let envpar = push_rel_context params env in let inst = if Declareops.inductive_is_polymorphic mib then @@ -173,10 +174,11 @@ let print_record env mind mib udecl = in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in + let nparamdecls = Context.Rel.length params in let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in - let cstrtype = hnf_prod_applist env cstrtypes.(0) args in + let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0)) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index fc94a1013..833e34c33 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -146,6 +146,7 @@ let cur_pstate () = | [] -> raise NoCurrentProof let give_me_the_proof () = (cur_pstate ()).proof +let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None let get_current_proof_name () = (cur_pstate ()).pid let with_current_proof f = diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 27e99f218..29445a746 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -24,6 +24,7 @@ val discard : Names.Id.t Loc.located -> unit val discard_current : unit -> unit val discard_all : unit -> unit +val give_me_the_proof_opt : unit -> Proof.t option exception NoCurrentProof val give_me_the_proof : unit -> Proof.t (** @raise NoCurrentProof when outside proof mode. *) diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index 10b42f7e9..81637f143 100644 --- a/stm/proofworkertop.ml +++ b/stm/proofworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ()) diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml index a1fe50c63..7862f2f44 100644 --- a/stm/queryworkertop.ml +++ b/stm/queryworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ()) diff --git a/stm/stm.ml b/stm/stm.ml index 6c956e134..92587b8ea 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2106,8 +2106,7 @@ and Reach : sig end = struct (* {{{ *) let async_policy () = - let open Flags in - if is_universe_polymorphism () then false + if Flags.is_universe_polymorphism () then false else if VCS.is_interactive () = `Yes then (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy) else diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml index 17f90b7b1..22b45a9be 100644 --- a/stm/tacworkertop.ml +++ b/stm/tacworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ()) diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 704119186..d606f19bf 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -15,8 +15,8 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let loop init args = - let args = parse args in +let loop init _coq_args extra_args = + let args = parse extra_args in Flags.quiet := true; init (); CoqworkmgrApi.init !async_proofs_worker_priority; diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli index da2e6fe0c..c42b48a28 100644 --- a/stm/workerLoop.mli +++ b/stm/workerLoop.mli @@ -9,4 +9,4 @@ (* Default priority *) val async_proofs_worker_priority : CoqworkmgrApi.priority ref -val loop : (unit -> unit) -> string list -> string list +val loop : (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> string list diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9011c4425..29a30b4a2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2154,11 +2154,11 @@ let keep hyps = and [a1..an:A1..An(a1..an-1)] such that the goal is [G(a1..an)], this generalizes [hyps |- goal] into [hyps |- T] *) -let apply_type newcl args = +let apply_type ~typecheck newcl args = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in - Refine.refine ~typecheck:false begin fun sigma -> + Refine.refine ~typecheck begin fun sigma -> let newcl = nf_betaiota env sigma newcl (* As in former Logic.refine *) in let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true ~store newcl in @@ -2889,7 +2889,7 @@ let generalize_dep ?(with_let=false) c = let args = Context.Named.to_instance mkVar to_quantify_rev in tclTHENLIST [ Proofview.Unsafe.tclEVARS evd; - apply_type cl'' (if Option.is_empty body then c::args else args); + apply_type ~typecheck:false cl'' (if Option.is_empty body then c::args else args); clear (List.rev tothin')] end @@ -2903,7 +2903,7 @@ let generalize_gen_let lconstr = Proofview.Goal.enter begin fun gl -> let (evd, _) = Typing.type_of env evd newcl in let map ((_, c, b),_) = if Option.is_empty b then Some c else None in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) - (apply_type newcl (List.map_filter map lconstr)) + (apply_type ~typecheck:false newcl (List.map_filter map lconstr)) end let new_generalize_gen_let lconstr = @@ -4277,7 +4277,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) (Tacticals.New.tclTHENLIST [ (* Generalize dependent hyps (but not args) *) - if deps = [] then Proofview.tclUNIT () else apply_type tmpcl deps_cstr; + if deps = [] then Proofview.tclUNIT () else apply_type ~typecheck:false tmpcl deps_cstr; (* side-conditions in elim (resp case) schemes come last (resp first) *) induct_tac elim; Tacticals.New.tclMAP expand_hyp toclear; diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 483e790e5..74415f8d0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -185,7 +185,7 @@ val revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) -val apply_type : constr -> constr list -> unit Proofview.tactic +val apply_type : typecheck:bool -> constr -> constr list -> unit Proofview.tactic val bring_hyps : named_context -> unit Proofview.tactic val apply : constr -> unit Proofview.tactic diff --git a/test-suite/bugs/closed/6677.v b/test-suite/bugs/closed/6677.v new file mode 100644 index 000000000..99e47bb87 --- /dev/null +++ b/test-suite/bugs/closed/6677.v @@ -0,0 +1,5 @@ +Set Universe Polymorphism. + +Definition T@{i} := Type@{i}. +Fail Definition U@{i} := (T@{i} <: Type@{i}). +Fail Definition eqU@{i j} : @eq T@{j} U@{i} T@{i} := eq_refl. diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject b/test-suite/coq-makefile/emptyprefix/_CoqProject new file mode 100644 index 000000000..5678a8edb --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject @@ -0,0 +1,11 @@ +-R theories "" +-R src "" +-I src +-arg "-w default" + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject.sub b/test-suite/coq-makefile/emptyprefix/_CoqProject.sub new file mode 100644 index 000000000..90ac541e0 --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject.sub @@ -0,0 +1,3 @@ +-R ../theories "" +-I ../src +testsub.v diff --git a/test-suite/coq-makefile/emptyprefix/run.sh b/test-suite/coq-makefile/emptyprefix/run.sh new file mode 100755 index 000000000..a10e63b42 --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/run.sh @@ -0,0 +1,17 @@ +#!/usr/bin/env bash + +set -e + +. ../template/init.sh + +mv theories/sub theories2 + +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +make + +cp ../_CoqProject.sub theories2/_CoqProject +cd theories2 +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +make diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject new file mode 100644 index 000000000..69f47302e --- /dev/null +++ b/test-suite/coq-makefile/quick2vo/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/quick2vo/run.sh b/test-suite/coq-makefile/quick2vo/run.sh new file mode 100755 index 000000000..9e681223b --- /dev/null +++ b/test-suite/coq-makefile/quick2vo/run.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash +a=`uname` + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +# vio2vo is broken on Windows (#6720) +if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then + make quick2vo J=2 + test -f theories/test.vo + make validate +fi diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject new file mode 100644 index 000000000..69f47302e --- /dev/null +++ b/test-suite/coq-makefile/vio2vo/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/vio2vo/run.sh b/test-suite/coq-makefile/vio2vo/run.sh new file mode 100755 index 000000000..85656da41 --- /dev/null +++ b/test-suite/coq-makefile/vio2vo/run.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash +a=`uname` + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make quick +# vio2vo is broken on Windows (#6720) +if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then + make vio2vo J=2 + test -f theories/test.vo + make validate +fi diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index e912003f0..af202ea01 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,3 +1,7 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in "A -> list' A -> list' (A * A)%type". +Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x + +For foo: Argument scopes are [type_scope _] +For Foo: Argument scopes are [type_scope _] diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index 8db8956e3..8ff91268a 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -1,3 +1,7 @@ Fail Inductive list' (A:Set) : Set := | nil' : list' A | cons' : A -> list' A -> list' (A*A). + +(* Check printing of let-ins *) +Inductive foo (A : Type) (x : A) (y := x) := Foo. +Print foo. diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 1fb3abfe4..e05762477 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -124,3 +124,13 @@ Inductive Mut1 A := with Mut2 A := | Base2 : Type -> Mut2 A | Node2 : Mut1 A -> Mut2 A. + +(* If we don't reduce T while inferring cumulativity for the + constructor we will see a Rel and believe i is irrelevant. *) +Inductive withparams@{i j} (T:=Type@{i}:Type@{j}) := mkwithparams : T -> withparams. + +Definition withparams_co@{i i' j|i < i', i' < j} : withparams@{i j} -> withparams@{i' j} + := fun x => x. + +Fail Definition withparams_not_irr@{i i' j|i' < i, i' < j} : withparams@{i j} -> withparams@{i' j} + := fun x => x. diff --git a/theories/.dir-locals.el b/theories/.dir-locals.el deleted file mode 100644 index 4e8830f6c..000000000 --- a/theories/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -((coq-mode . ((eval . (let ((default-directory (locate-dominating-file - buffer-file-name ".dir-locals.el"))) - (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq")) - (setq-local coq-prog-name (expand-file-name "../bin/coqtop"))))))) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index ca02c983d..727fd3ec3 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -34,11 +34,10 @@ LOCAL := $(COQMF_LOCAL) COQLIB := $(COQMF_COQLIB) DOCDIR := $(COQMF_DOCDIR) OCAMLFIND := $(COQMF_OCAMLFIND) -CAMLP4 := $(COQMF_CAMLP4) -CAMLP4O := $(COQMF_CAMLP4O) -CAMLP4BIN := $(COQMF_CAMLP4BIN) -CAMLP4LIB := $(COQMF_CAMLP4LIB) -CAMLP4OPTIONS := $(COQMF_CAMLP4OPTIONS) +CAMLP5O := $(COQMF_CAMLP5O) +CAMLP5BIN := $(COQMF_CAMLP5BIN) +CAMLP5LIB := $(COQMF_CAMLP5LIB) +CAMLP5OPTIONS := $(COQMF_CAMLP5OPTIONS) CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) @@ -169,7 +168,8 @@ endif COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) COQCHKFLAGS?=-silent -o $(COQLIBS) -COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML) +COQDOCFLAGS?=-interpolate -utf8 +COQDOCLIBS?=$(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that # generated this makefile @@ -178,24 +178,20 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB) # ocamldoc fails with unknown argument otherwise CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) # FIXME This should be generated by Coq GRAMMARS:=grammar.cma -ifeq ($(CAMLP4),camlp5) -CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo -else -CAMLP4EXTEND= -endif +CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) ifeq (,$(CAMLLIB)) PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") else -PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' +PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl' endif ifneq (,$(TIMING)) @@ -381,7 +377,7 @@ bytefiles: $(CMOFILES) $(CMAFILES) optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) .PHONY: optfiles -# FIXME, see Ralph's bugreport +# FIXME, see Ralf's bugreport quick: $(VOFILES:.vo=.vio) .PHONY: quick @@ -390,6 +386,18 @@ vio2vo: -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) .PHONY: vio2vo +quick2vo: + $(HIDE)make -j $(J) quick + $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ + viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ + if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ + done); \ + echo "VIO2VO: $$VIOFILES"; \ + if [ -n "$$VIOFILES" ]; then \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \ + fi +.PHONY: quick2vo + checkproofs: $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) @@ -739,11 +747,10 @@ printenv:: @echo 'COQLIB = $(COQLIB)' @echo 'DOCDIR = $(DOCDIR)' @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'CAMLP4 = $(CAMLP4)' - @echo 'CAMLP4O = $(CAMLP4O)' - @echo 'CAMLP4BIN = $(CAMLP4BIN)' - @echo 'CAMLP4LIB = $(CAMLP4LIB)' - @echo 'CAMLP4OPTIONS = $(CAMLP4OPTIONS)' + @echo 'CAMLP5O = $(CAMLP5O)' + @echo 'CAMLP5BIN = $(CAMLP5BIN)' + @echo 'CAMLP5LIB = $(CAMLP5LIB)' + @echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)' @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 091869407..1e1862220 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -124,7 +124,7 @@ let read_whole_file s = close_in ic; Buffer.contents b -let quote s = if String.contains s ' ' then "'" ^ s ^ "'" else s +let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s let generate_makefile oc conf_file local_file args project = let makefile_template = diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml new file mode 100644 index 000000000..5b73471c5 --- /dev/null +++ b/toplevel/coqargs.ml @@ -0,0 +1,575 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +let warning s = Flags.(with_option warn Feedback.msg_warning (Pp.strbrk s)) + +let fatal_error ?extra exn = + Topfmt.print_err_exn ?extra exn; + let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in + exit exit_code + +let error_missing_arg s = + prerr_endline ("Error: extra argument expected after option "^s); + prerr_endline "See -help for the syntax of supported options"; + exit 1 + +(******************************************************************************) +(* Imperative effects! This must be fixed at some point. *) +(******************************************************************************) +let set_worker_id opt s = + assert (s <> "master"); + Flags.async_proofs_worker_id := s + +let set_type_in_type () = + let typing_flags = Environ.typing_flags (Global.env ()) in + Global.set_typing_flags { typing_flags with Declarations.check_universes = false } + +(******************************************************************************) + +type compilation_mode = BuildVo | BuildVio | Vio2Vo +type color = [`ON | `AUTO | `OFF] + +type coq_cmdopts = { + + load_init : bool; + load_rcfile : bool; + rcfile : string option; + + ml_includes : string list; + vo_includes : (string * Names.DirPath.t * bool) list; + vo_requires : (string * string option * bool option) list; + (* None = No Import; Some false = Import; Some true = Export *) + + (* XXX: Fusion? *) + batch_mode : bool; + compilation_mode : compilation_mode; + + toplevel_name : Names.DirPath.t; + toploop : string option; + + compile_list: (string * bool) list; (* bool is verbosity *) + compilation_output_name : string option; + + load_vernacular_list : (string * bool) list; + + vio_checking: bool; + vio_tasks : (int list * string) list; + vio_files : string list; + vio_files_j : int; + + color : color; + + impredicative_set : Declarations.set_predicativity; + stm_flags : Stm.AsyncOpts.stm_opt; + debug : bool; + time : bool; + + filter_opts : bool; + + glob_opt : bool; + + memory_stat : bool; + print_tags : bool; + print_where : bool; + print_config: bool; + output_context : bool; + + inputstate : string option; + outputstate : string option; + +} + +let init_args = { + + load_init = true; + load_rcfile = true; + rcfile = None; + + ml_includes = []; + vo_includes = []; + vo_requires = []; + + batch_mode = false; + compilation_mode = BuildVo; + + toplevel_name = Names.(DirPath.make [Id.of_string "Top"]); + toploop = None; + + compile_list = []; + compilation_output_name = None; + + load_vernacular_list = []; + + vio_checking = false; + vio_tasks = []; + vio_files = []; + vio_files_j = 0; + + color = `AUTO; + + impredicative_set = Declarations.PredicativeSet; + stm_flags = Stm.AsyncOpts.default_opts; + debug = false; + time = false; + + filter_opts = false; + + glob_opt = false; + + memory_stat = false; + print_tags = false; + print_where = false; + print_config = false; + output_context = false; + + inputstate = None; + outputstate = None; +} + +(******************************************************************************) +(* Functional arguments *) +(******************************************************************************) +let add_ml_include opts s = + { opts with ml_includes = s :: opts.ml_includes } + +let add_vo_include opts d p implicit = + let p = Libnames.dirpath_of_string p in + { opts with vo_includes = (d, p, implicit) :: opts.vo_includes } + +let add_vo_require opts d p export = + { opts with vo_requires = (d, p, export) :: opts.vo_requires } + +let add_compat_require opts v = + match v with + | Flags.V8_5 -> add_vo_require opts "Coq.Compat.Coq85" None (Some false) + | Flags.V8_6 -> add_vo_require opts "Coq.Compat.Coq86" None (Some false) + | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false) + | Flags.VOld | Flags.Current -> opts + +let set_batch_mode opts = + Flags.quiet := true; + System.trust_file_cache := false; + { opts with batch_mode = true } + +let add_compile opts verbose s = + let opts = set_batch_mode opts in + if not opts.glob_opt then Dumpglob.dump_to_dotglob (); + (** make the file name explicit; needed not to break up Coq loadpath stuff. *) + let s = + let open Filename in + if is_implicit s + then concat current_dir_name s + else s + in + { opts with compile_list = (s,verbose) :: opts.compile_list } + +let add_load_vernacular opts verb s = + { opts with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.load_vernacular_list } + +let add_vio_task opts f = + let opts = set_batch_mode opts in + { opts with vio_tasks = f :: opts.vio_tasks } + +let add_vio_file opts f = + let opts = set_batch_mode opts in + { opts with vio_files = f :: opts.vio_files } + +let set_vio_checking_j opts opt j = + try { opts with vio_files_j = int_of_string j } + with Failure _ -> + prerr_endline ("The first argument of " ^ opt ^ " must the number"); + prerr_endline "of concurrent workers to be used (a positive integer)."; + prerr_endline "Makefiles generated by coq_makefile should be called"; + prerr_endline "setting the J variable like in 'make vio2vo J=3'"; + exit 1 + +(** Options for proof general *) +let set_emacs opts = + if not (Option.is_empty opts.toploop) then + CErrors.user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop"); + Coqloop.print_emacs := true; + Printer.enable_goal_tags_printing := true; + { opts with color = `OFF } + +let set_color opts = function +| "yes" | "on" -> { opts with color = `ON } +| "no" | "off" -> { opts with color = `OFF } +| "auto" -> { opts with color = `AUTO } +| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1 + +let warn_deprecated_inputstate = + CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" + (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") + +let set_inputstate opts s = + warn_deprecated_inputstate (); + { opts with inputstate = Some s } + +let warn_deprecated_outputstate = + CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated" + (fun () -> + Pp.strbrk "The outputstate option is deprecated and discouraged.") + +let set_outputstate opts s = + warn_deprecated_outputstate (); + { opts with outputstate = Some s } + +let exitcode opts = if opts.filter_opts then 2 else 0 + +(******************************************************************************) +(* Parsing helpers *) +(******************************************************************************) +let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) + +let get_bool opt = function + | "yes" | "on" -> true + | "no" | "off" -> false + | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 + +let get_int opt n = + try int_of_string n + with Failure _ -> + prerr_endline ("Error: integer expected after option "^opt); exit 1 + +let get_float opt n = + try float_of_string n + with Failure _ -> + prerr_endline ("Error: float expected after option "^opt); exit 1 + +let get_host_port opt s = + match CString.split ':' s with + | [host; portr; portw] -> + Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) + | ["stdfds"] -> Some Spawned.AnonPipe + | _ -> + prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt); + exit 1 + +let get_error_resilience opt = function + | "on" | "all" | "yes" -> `All + | "off" | "no" -> `None + | s -> `Only (CString.split ',' s) + +let get_priority opt s = + try CoqworkmgrApi.priority_of_string s + with Invalid_argument _ -> + prerr_endline ("Error: low/high expected after "^opt); exit 1 + +let get_async_proofs_mode opt = let open Stm.AsyncOpts in function + | "no" | "off" -> APoff + | "yes" | "on" -> APon + | "lazy" -> APonLazy + | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 + +let get_cache opt = function + | "force" -> Some Stm.AsyncOpts.Force + | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 + +let is_not_dash_option = function + | Some f when String.length f > 0 && f.[0] <> '-' -> true + | _ -> false + +let rec add_vio_args peek next oval = + if is_not_dash_option (peek ()) then + let oval = add_vio_file oval (next ()) in + add_vio_args peek next oval + else oval + +let get_native_name s = + (* We ignore even critical errors because this mode has to be super silent *) + try + String.concat "/" [Filename.dirname s; + Nativelib.output_dir; Library.native_name_from_filename s] + with _ -> "" + +(*s Parsing of the command line. + We no longer use [Arg.parse], in order to use share [Usage.print_usage] + between coqtop and coqc. *) + +let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem" + (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned") + +exception NoCoqLib + +let usage batch = + begin + try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) + with NoCoqLib -> usage_no_coqlib () + end; + let lp = Coqinit.toplevel_init_load_path () in + (* Necessary for finding the toplevels below *) + List.iter Mltop.add_coq_path lp; + if batch then Usage.print_usage_coqc () + else begin + Mltop.load_ml_objects_raw_rex + (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$")); + Usage.print_usage_coqtop () + end + +(* Main parsing routine *) +let parse_args arglist : coq_cmdopts * string list = + let args = ref arglist in + let extras = ref [] in + let rec parse oval = match !args with + | [] -> + (oval, List.rev !extras) + | opt :: rem -> + args := rem; + let next () = match !args with + | x::rem -> args := rem; x + | [] -> error_missing_arg opt + in + let peek_next () = match !args with + | x::_ -> Some x + | [] -> None + in + let noval = begin match opt with + + (* Complex options with many args *) + |"-I"|"-include" -> + begin match rem with + | d :: rem -> + args := rem; + add_ml_include oval d + | [] -> error_missing_arg opt + end + |"-Q" -> + begin match rem with + | d :: p :: rem -> + args := rem; + add_vo_include oval d p false + | _ -> error_missing_arg opt + end + |"-R" -> + begin match rem with + | d :: p :: rem -> + args := rem; + add_vo_include oval d p true + | _ -> error_missing_arg opt + end + + (* Options with two arg *) + |"-check-vio-tasks" -> + let tno = get_task_list (next ()) in + let tfile = next () in + add_vio_task oval (tno,tfile) + + |"-schedule-vio-checking" -> + let oval = { oval with vio_checking = true } in + let oval = set_vio_checking_j oval opt (next ()) in + let oval = add_vio_file oval (next ()) in + add_vio_args peek_next next oval + + |"-schedule-vio2vo" -> + let oval = set_vio_checking_j oval opt (next ()) in + let oval = add_vio_file oval (next ()) in + add_vio_args peek_next next oval + + (* Options with one arg *) + |"-coqlib" -> + Flags.coqlib_spec := true; + Flags.coqlib := (next ()); + oval + + |"-async-proofs" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next()) + }} + |"-async-proofs-j" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ())) + }} + |"-async-proofs-cache" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ()) + }} + + |"-async-proofs-tac-j" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ())) + }} + + |"-async-proofs-worker-priority" -> + WorkerLoop.async_proofs_worker_priority := get_priority opt (next ()); + oval + + |"-async-proofs-private-flags" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_private_flags = Some (next ()); + }} + + |"-async-proofs-tactic-error-resilience" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ()) + }} + + |"-async-proofs-command-error-resilience" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ()) + }} + + |"-async-proofs-delegation-threshold" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ()) + }} + + |"-worker-id" -> set_worker_id opt (next ()); oval + + |"-compat" -> + let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in + Flags.compat_version := v; + add_compat_require oval v + + |"-compile" -> + add_compile oval false (next ()) + + |"-compile-verbose" -> + add_compile oval true (next ()) + + |"-dump-glob" -> + Dumpglob.dump_into_file (next ()); + { oval with glob_opt = true } + + |"-feedback-glob" -> + Dumpglob.feedback_glob (); oval + + |"-exclude-dir" -> + System.exclude_directory (next ()); oval + + |"-init-file" -> + { oval with rcfile = Some (next ()); } + + |"-inputstate"|"-is" -> + set_inputstate oval (next ()) + + |"-outputstate" -> + set_outputstate oval (next ()) + + |"-load-ml-object" -> + Mltop.dir_ml_load (next ()); oval + + |"-load-ml-source" -> + Mltop.dir_ml_use (next ()); oval + + |"-load-vernac-object" -> + add_vo_require oval (next ()) None None + + |"-load-vernac-source"|"-l" -> + add_load_vernacular oval false (next ()) + + |"-load-vernac-source-verbose"|"-lv" -> + add_load_vernacular oval true (next ()) + + |"-print-mod-uid" -> + let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 + + |"-profile-ltac-cutoff" -> + Flags.profile_ltac := true; + Flags.profile_ltac_cutoff := get_float opt (next ()); + oval + + |"-require" -> add_vo_require oval (next ()) None (Some false) + + |"-top" -> + let topname = Libnames.dirpath_of_string (next ()) in + if Names.DirPath.is_empty topname then + CErrors.user_err Pp.(str "Need a non empty toplevel module name"); + { oval with toplevel_name = topname } + + |"-main-channel" -> + Spawned.main_channel := get_host_port opt (next()); oval + + |"-control-channel" -> + Spawned.control_channel := get_host_port opt (next()); oval + + |"-vio2vo" -> + let oval = add_compile oval false (next ()) in + { oval with compilation_mode = Vio2Vo } + + |"-toploop" -> + if !Coqloop.print_emacs then + CErrors.user_err Pp.(str "Flags -toploop and -emacs are incompatible"); + { oval with toploop = Some (next ()) } + + |"-w" | "-W" -> + let w = next () in + if w = "none" then + (CWarnings.set_flags w; oval) + else + let w = CWarnings.get_flags () ^ "," ^ w in + CWarnings.set_flags (CWarnings.normalize_flags_string w); + oval + + |"-o" -> { oval with compilation_output_name = Some (next()) } + + (* Options with zero arg *) + |"-async-queries-always-delegate" + |"-async-proofs-always-delegate" + |"-async-proofs-full" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_full = true; + }} + |"-async-proofs-never-reopen-branch" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_never_reopen_branch = true + }} + |"-batch" -> set_batch_mode oval + |"-test-mode" -> Flags.test_mode := true; oval + |"-beautify" -> Flags.beautify := true; oval + |"-boot" -> Flags.boot := true; { oval with load_rcfile = false; } + |"-bt" -> Backtrace.record_backtrace true; oval + |"-color" -> set_color oval (next ()) + |"-config"|"--config" -> { oval with print_config = true } + |"-debug" -> Coqinit.set_debug (); oval + |"-stm-debug" -> Stm.stm_debug := true; oval + |"-emacs" -> set_emacs oval + |"-filteropts" -> { oval with filter_opts = true } + |"-ideslave" -> + if !Coqloop.print_emacs then + CErrors.user_err Pp.(str "Flags -ideslave and -emacs are incompatible"); + Flags.ide_slave := true; + { oval with toploop = Some "coqidetop" } + + |"-impredicative-set" -> + { oval with impredicative_set = Declarations.ImpredicativeSet } + |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval + |"-m"|"--memory" -> { oval with memory_stat = true } + |"-noinit"|"-nois" -> { oval with load_init = false } + |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with glob_opt = true } + |"-native-compiler" -> + if not Coq_config.native_compiler then + warning "Native compilation was disabled at configure time." + else Flags.output_native_objects := true; oval + |"-output-context" -> { oval with output_context = true } + |"-profile-ltac" -> Flags.profile_ltac := true; oval + |"-q" -> { oval with load_rcfile = false; } + |"-quiet"|"-silent" -> + Flags.quiet := true; + Flags.make_warn false; + oval + |"-quick" -> { oval with compilation_mode = BuildVio } + |"-list-tags" -> { oval with print_tags = true } + |"-time" -> { oval with time = true } + |"-type-in-type" -> set_type_in_type (); oval + |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) + |"-where" -> { oval with print_where = true } + |"-h"|"-H"|"-?"|"-help"|"--help" -> usage oval.batch_mode; oval + |"-v"|"--version" -> Usage.version (exitcode oval) + |"-print-version"|"--print-version" -> + Usage.machine_readable_version (exitcode oval) + + (* Unknown option *) + | s -> + extras := s :: !extras; + oval + end in + parse noval + in + try + parse init_args + with any -> fatal_error any diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli new file mode 100644 index 000000000..8ee1a8f55 --- /dev/null +++ b/toplevel/coqargs.mli @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type compilation_mode = BuildVo | BuildVio | Vio2Vo +type color = [`ON | `AUTO | `OFF] + +type coq_cmdopts = { + + load_init : bool; + load_rcfile : bool; + rcfile : string option; + + ml_includes : string list; + vo_includes : (string * Names.DirPath.t * bool) list; + vo_requires : (string * string option * bool option) list; + + (* Fuse these two? Currently, [batch_mode] is only used to + distinguish coqc / coqtop in help display. *) + batch_mode : bool; + compilation_mode : compilation_mode; + + toplevel_name : Names.DirPath.t; + toploop : string option; + + compile_list: (string * bool) list; (* bool is verbosity *) + compilation_output_name : string option; + + load_vernacular_list : (string * bool) list; + + vio_checking: bool; + vio_tasks : (int list * string) list; + vio_files : string list; + vio_files_j : int; + + color : color; + + impredicative_set : Declarations.set_predicativity; + stm_flags : Stm.AsyncOpts.stm_opt; + debug : bool; + time : bool; + + filter_opts : bool; + + glob_opt : bool; + + memory_stat : bool; + print_tags : bool; + print_where : bool; + print_config: bool; + output_context : bool; + + inputstate : string option; + outputstate : string option; + +} + +val parse_args : string list -> coq_cmdopts * string list +val exitcode : coq_cmdopts -> int diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 10205964a..d8aaf3db8 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -20,21 +20,15 @@ let set_debug () = does not exist. *) let rcdefaultname = "coqrc" -let rcfile = ref "" -let rcfile_specified = ref false -let set_rcfile s = rcfile := s; rcfile_specified := true -let load_rc = ref true -let no_load_rc () = load_rc := false - -let load_rcfile ~time doc sid = - if !load_rc then +let load_rcfile ~rcfile ~time ~state = try - if !rcfile_specified then - if CUnix.file_readable_p !rcfile then - Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid !rcfile - else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) - else + match rcfile with + | Some rcfile -> + if CUnix.file_readable_p rcfile then + Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state rcfile + else raise (Sys_error ("Cannot read rcfile: "^ rcfile)) + | None -> try let warn x = Feedback.msg_warning (str x) in let inferedrc = List.find CUnix.file_readable_p [ @@ -43,8 +37,8 @@ let load_rcfile ~time doc sid = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid inferedrc - with Not_found -> doc, sid + Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state inferedrc + with Not_found -> state (* Flags.if_verbose mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ @@ -54,9 +48,6 @@ let load_rcfile ~time doc sid = let reraise = CErrors.push reraise in let () = Feedback.msg_info (str"Load of rcfile failed.") in iraise reraise - else - (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); - doc, sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml = @@ -77,13 +68,6 @@ let build_userlib_path ~unix_path = } } -(* Options -I, -I-as, and -R of the command line *) -let includes = ref [] -let push_include s alias implicit = - includes := (s, alias, implicit) :: !includes -let ml_includes = ref [] -let push_ml_include s = ml_includes := s :: !ml_includes - let ml_path_if c p = let open Mltop in let f x = { recursive = false; path_spec = MlPath x } in @@ -128,17 +112,7 @@ let libs_init_load_path ~load_init = coq_path = Libnames.default_root_prefix; implicit = false; has_ml = AddTopML } - } ] @ - - (* additional loadpaths, given with options -Q and -R *) - List.map - (fun (unix_path, coq_path, implicit) -> - { recursive = true; - path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } }) - (List.rev !includes) @ - - (* additional ml directories, given with option -I *) - List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev !ml_includes) + } ] (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 0d2da84bb..14f39170c 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -10,19 +10,12 @@ val set_debug : unit -> unit -val set_rcfile : string -> unit - -val no_load_rc : unit -> unit -val load_rcfile : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t - -val push_include : string -> Names.DirPath.t -> bool -> unit -(** [push_include phys_path log_path implicit] *) - -val push_ml_include : string -> unit +val load_rcfile : rcfile:(string option) -> time:bool -> state:Vernac.State.t -> Vernac.State.t val init_ocaml_path : unit -> unit (* LoadPath for toploop toplevels *) val toplevel_init_load_path : unit -> Mltop.coq_path list + (* LoadPath for Coq user libraries *) val libs_init_load_path : load_init:bool -> Mltop.coq_path list diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index aade101a4..ae0b94476 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -258,8 +258,9 @@ let rec discard_to_dot () = | Stm.End_of_input -> raise Stm.End_of_input | e when CErrors.noncritical e -> () -let read_sentence ~doc sid input = - try Stm.parse_sentence ~doc sid input +let read_sentence ~state input = + let open Vernac.State in + try Stm.parse_sentence ~doc:state.doc state.sid input with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); @@ -300,19 +301,20 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in is caught and handled (i.e. not re-raised). *) -let do_vernac ~time doc sid = +let do_vernac ~time ~state = + let open Vernac.State in top_stderr (fnl()); - if !print_emacs then top_stderr (str (top_buffer.prompt doc)); + if !print_emacs then top_stderr (str (top_buffer.prompt state.doc)); resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in - Vernac.process_expr ~time doc sid (read_sentence ~doc sid (fst input)) + Vernac.process_expr ~time ~state (read_sentence ~state (fst input)) with | Stm.End_of_input | CErrors.Quit -> top_stderr (fnl ()); raise CErrors.Quit | CErrors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise CErrors.Drop - else (Feedback.msg_warning (str "There is no ML toplevel."); doc, sid) + else (Feedback.msg_warning (str "There is no ML toplevel."); state) (* Exception printing should be done by the feedback listener, however this is not yet ready so we rely on the exception for now. *) @@ -321,7 +323,7 @@ let do_vernac ~time doc sid = let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; - doc, sid + state (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -337,20 +339,21 @@ let loop_flush_all () = Format.pp_print_flush !Topfmt.std_ft (); Format.pp_print_flush !Topfmt.err_ft () -let rec loop ~time doc = +let rec loop ~time ~state = + let open Vernac.State in Sys.catch_break true; try - reset_input_buffer doc stdin top_buffer; + reset_input_buffer state.doc stdin top_buffer; (* Be careful to keep this loop tail-recursive *) - let rec vernac_loop doc sid = - let ndoc, nsid = do_vernac ~time doc sid in + let rec vernac_loop ~state = + let nstate = do_vernac ~time ~state in loop_flush_all (); - vernac_loop ndoc nsid + vernac_loop ~state:nstate (* We recover the current stateid, threading from the caller is not possible due exceptions. *) - in vernac_loop doc (Stm.get_current_state ~doc) + in vernac_loop ~state with - | CErrors.Drop -> doc + | CErrors.Drop -> state | CErrors.Quit -> exit 0 | any -> top_stderr (str "Anomaly: main loop exited with exception: " ++ @@ -358,4 +361,4 @@ let rec loop ~time doc = fnl() ++ str"Please report" ++ strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); - loop ~time doc + loop ~time ~state diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 09240ec82..1c1309051 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -31,9 +31,7 @@ val set_prompt : (unit -> string) -> unit val coqloop_feed : Feedback.feedback -> unit (** Parse and execute one vernac command. *) - -val do_vernac : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t +val do_vernac : time:bool -> state:Vernac.State.t -> Vernac.State.t (** Main entry point of Coq: read and execute vernac commands. *) - -val loop : time:bool -> Stm.doc -> Stm.doc +val loop : time:bool -> state:Vernac.State.t -> Vernac.State.t diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 400f7048d..26ede1834 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -7,8 +7,7 @@ (************************************************************************) open Pp -open CErrors -open Libnames +open Coqargs let () = at_exit flush_all @@ -31,68 +30,23 @@ let print_header () = let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) -let toploop = ref None - -let color : [`ON | `AUTO | `OFF] ref = ref `AUTO -let set_color = function -| "yes" | "on" -> color := `ON -| "no" | "off" -> color := `OFF -| "auto" -> color := `AUTO -| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1 - -let init_color () = - let has_color = match !color with - | `OFF -> false - | `ON -> true - | `AUTO -> - Terminal.has_style Unix.stdout && - Terminal.has_style Unix.stderr && - (* emacs compilation buffer does not support colors by default, - its TERM variable is set to "dumb". *) - try Sys.getenv "TERM" <> "dumb" with Not_found -> false - in - if has_color then begin - let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in - match colors with - | None -> - (** Default colors *) - Topfmt.init_terminal_output ~color:true - | Some "" -> - (** No color output *) - Topfmt.init_terminal_output ~color:false - | Some s -> - (** Overwrite all colors *) - Topfmt.clear_styles (); - Topfmt.parse_color_config s; - Topfmt.init_terminal_output ~color:true - end - else - Topfmt.init_terminal_output ~color:false - -let toploop_init = ref begin fun x -> - let () = init_color () in - let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in - x - end - (* Feedback received in the init stage, this is different as the STM will not be generally be initialized, thus stateid, etc... may be bogus. For now we just print to the console too *) let coqtop_init_feed = Coqloop.coqloop_feed let drop_last_doc = ref None -let measure_time = ref false (* Default toplevel loop *) -let console_toploop_run doc = +let console_toploop_run opts ~state = (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in if Dumpglob.dump () then begin Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; - let doc = Coqloop.loop ~time:!measure_time doc in + let state = Coqloop.loop ~time:opts.time ~state in (* Initialise and launch the Ocaml toplevel *) - drop_last_doc := Some doc; + drop_last_doc := Some state; Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); (* We let the feeder in place for users of Drop *) @@ -100,10 +54,7 @@ let console_toploop_run doc = let toploop_run = ref console_toploop_run -let output_context = ref false - let memory_stat = ref false - let print_memory_stat () = begin (* -m|--memory from the command-line *) if !memory_stat then @@ -124,133 +75,89 @@ let print_memory_stat () = let _ = at_exit print_memory_stat (******************************************************************************) -(* Engagement *) -(******************************************************************************) -let impredicative_set = ref Declarations.PredicativeSet -let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet -let set_type_in_type () = - let typing_flags = Environ.typing_flags (Global.env ()) in - Global.set_typing_flags { typing_flags with Declarations.check_universes = false } -let engage () = - Global.set_engagement !impredicative_set - -(******************************************************************************) -(* Interactive toplevel name *) -(******************************************************************************) -let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"]) -let toplevel_name = ref toplevel_default_name -let set_toplevel_name dir = - if Names.DirPath.is_empty dir then user_err Pp.(str "Need a non empty toplevel module name"); - toplevel_name := dir - -(******************************************************************************) (* Input/Output State *) (******************************************************************************) -let warn_deprecated_inputstate = - CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" - (fun () -> strbrk "The inputstate option is deprecated and discouraged.") - -let inputstate = ref "" -let set_inputstate s = - warn_deprecated_inputstate (); - inputstate:=s -let inputstate () = - if not (CString.is_empty !inputstate) then - let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in - States.intern_state fname - -let warn_deprecated_outputstate = - CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated" - (fun () -> - strbrk "The outputstate option is deprecated and discouraged.") - -let outputstate = ref "" -let set_outputstate s = - warn_deprecated_outputstate (); - outputstate:=s -let outputstate () = - if not (CString.is_empty !outputstate) then - let fname = CUnix.make_suffix !outputstate ".coq" in - States.extern_state fname +let inputstate opts = + Option.iter (fun istate_file -> + let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in + States.intern_state fname) opts.inputstate + +let outputstate opts = + Option.iter (fun ostate_file -> + let fname = CUnix.make_suffix ostate_file ".coq" in + States.extern_state fname) opts.outputstate (******************************************************************************) (* Interactive Load File Simulation *) (******************************************************************************) -let load_vernacular_list = ref ([] : (string * bool) list) - -let add_load_vernacular verb s = - load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list - -let load_vernacular ~time doc sid = +let load_vernacular opts ~state = List.fold_left - (fun (doc,sid) (f_in, verbosely) -> + (fun state (f_in, verbosely) -> let s = Loadpath.locate_file f_in in - if !Flags.beautify then - Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid) f_in - else - Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid s) - (doc, sid) (List.rev !load_vernacular_list) - -let load_init_vernaculars ~time doc sid = - let doc, sid = Coqinit.load_rcfile ~time doc sid in - load_vernacular ~time doc sid + (* Should make the beautify logic clearer *) + let load_vernac f = Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true ~state f in + if !Flags.beautify + then Flags.with_option Flags.beautify_file load_vernac f_in + else load_vernac s + ) state (List.rev opts.load_vernacular_list) + +let load_init_vernaculars opts ~state = + let state = if opts.load_rcfile then + Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time ~state + else begin + Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); + state + end in + + load_vernacular opts ~state (******************************************************************************) -(* Required Modules *) +(* Startup LoadPath and Modules *) (******************************************************************************) -let set_include d p implicit = - let p = dirpath_of_string p in - Coqinit.push_include d p implicit +(* prelude_data == From Coq Require Export Prelude. *) +let prelude_data = "Prelude", Some "Coq", Some true -(* None = No Import; Some false = Import; Some true = Export *) -let require_list = ref ([] : (string * string option * bool option) list) -let add_require s = require_list := s :: !require_list +let require_libs opts = + if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires -let load_init = ref true +let cmdline_load_path opts = + let open Mltop in + (* loadpaths given by options -Q and -R *) + List.map + (fun (unix_path, coq_path, implicit) -> + { recursive = true; + path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } }) + (List.rev opts.vo_includes) @ -(* From Coq Require Import Prelude. *) -let prelude_data = "Prelude", Some "Coq", Some true + (* additional ml directories, given with option -I *) + List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev opts.ml_includes) -let require_libs () = - if !load_init then prelude_data :: !require_list else !require_list - -let add_compat_require v = - match v with - | Flags.V8_5 -> add_require ("Coq.Compat.Coq85", None, Some false) - | Flags.V8_6 -> add_require ("Coq.Compat.Coq86", None, Some false) - | Flags.V8_7 -> add_require ("Coq.Compat.Coq87", None, Some false) - | Flags.VOld | Flags.Current -> () +let build_load_path opts = + Coqinit.libs_init_load_path ~load_init:opts.load_init @ + cmdline_load_path opts (******************************************************************************) -(* File Compilation *) +(* Fatal Errors *) (******************************************************************************) -let glob_opt = ref false - -let compile_list = ref ([] : (bool * string) list) - -type compilation_mode = BuildVo | BuildVio | Vio2Vo -let compilation_mode = ref BuildVo -let compilation_output_name = ref None - -let batch_mode = ref false -let set_batch_mode () = - System.trust_file_cache := false; - batch_mode := true - -let add_compile verbose s = - set_batch_mode (); - Flags.quiet := true; - if not !glob_opt then Dumpglob.dump_to_dotglob (); - (** make the file name explicit; needed not to break up Coq loadpath stuff. *) - let s = - let open Filename in - if is_implicit s - then concat current_dir_name s - else s +(** Prints info which is either an error or an anomaly and then exits + with the appropriate error code *) +let fatal_error msg = + Topfmt.std_logger Feedback.Error msg; + flush_all (); + exit 1 + +let fatal_error_exn ?extra exn = + Topfmt.print_err_exn ?extra exn; + flush_all (); + let exit_code = + if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in - compile_list := (verbose,s) :: !compile_list + exit exit_code +(******************************************************************************) +(* File Compilation *) +(******************************************************************************) let warn_file_no_extension = CWarnings.create ~name:"file-no-extension" ~category:"filesystem" (fun (f,ext) -> @@ -268,16 +175,11 @@ let ensure_ext ext f = let chop_extension f = try Filename.chop_extension f with _ -> f -let compile_error msg = - Topfmt.std_logger Feedback.Error msg; - flush_all (); - exit 1 - let ensure_bname src tgt = let src, tgt = Filename.basename src, Filename.basename tgt in let src, tgt = chop_extension src, chop_extension tgt in if src <> tgt then - compile_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + fatal_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ str "Source: " ++ str src ++ fnl () ++ str "Target: " ++ str tgt) @@ -289,25 +191,24 @@ let ensure_vio v vio = ensure ".vio" v vio let ensure_exists f = if not (Sys.file_exists f) then - compile_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) - -let top_stm_options = ref Stm.AsyncOpts.default_opts + fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) (* Compile a vernac file *) -let compile ~time ~verbosely ~f_in ~f_out = +let compile opts ~verbosely ~f_in ~f_out = + let open Vernac.State in let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in if not (CList.is_empty pfs) then - compile_error (str "There are pending proofs: " + fatal_error (str "There are pending proofs: " ++ (pfs |> List.rev |> prlist_with_sep pr_comma Names.Id.print) ++ str ".") in - let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in - let require_libs = require_libs () in - let stm_options = !top_stm_options in - match !compilation_mode with + let iload_path = build_load_path opts in + let require_libs = require_libs opts in + let stm_options = opts.stm_flags in + match opts.compilation_mode with | BuildVo -> Flags.record_aux_file := true; let long_f_dot_v = ensure_v f_in in @@ -319,21 +220,20 @@ let compile ~time ~verbosely ~f_in ~f_out = let doc, sid = Stm.(new_doc { doc_type = VoDoc long_f_dot_vo; - iload_path; - require_libs; - stm_options; + iload_path; require_libs; stm_options; }) in - let doc, sid = load_init_vernaculars ~time doc sid in - let ldir = Stm.get_ldir ~doc in + let state = { doc; sid; proof = None } in + let state = load_init_vernaculars opts ~state in + let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) ~v_file:long_f_dot_v); Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); let wall_clock1 = Unix.gettimeofday () in - let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in - let _doc = Stm.join ~doc in + let state = Vernac.load_vernac ~time:opts.time ~verbosely ~check:true ~interactive:false ~state long_f_dot_v in + let _doc = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); @@ -354,18 +254,27 @@ let compile ~time ~verbosely ~f_in ~f_out = | None -> long_f_dot_v ^ "io" | Some f -> ensure_vio long_f_dot_v f in + (* We need to disable error resiliency, otherwise some errors + will be ignored in batch mode. c.f. #6707 + + This is not necessary in the vo case as it fully checks the + document anyways. *) + let stm_options = let open Stm.AsyncOpts in + { stm_options with + async_proofs_cmd_error_resilience = false; + async_proofs_tac_error_resilience = `None; + } in + let doc, sid = Stm.(new_doc { doc_type = VioDoc long_f_dot_vio; - iload_path; - require_libs; - stm_options; + iload_path; require_libs; stm_options; }) in - let doc, sid = load_init_vernaculars ~time doc sid in - - let ldir = Stm.get_ldir ~doc in - let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in - let doc = Stm.finish ~doc in + let state = { doc; sid; proof = None } in + let state = load_init_vernaculars opts ~state in + let ldir = Stm.get_ldir ~doc:state.doc in + let state = Vernac.load_vernac ~time:opts.time ~verbosely ~check:false ~interactive:false ~state long_f_dot_v in + let doc = Stm.finish ~doc:state.doc in check_pending_proofs (); let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in Stm.reset_task_queue () @@ -379,91 +288,96 @@ let compile ~time ~verbosely ~f_in ~f_out = let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv sum lib univs proofs -let compile ~time ~verbosely ~f_in ~f_out = +let compile opts ~verbosely ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile ~time ~verbosely ~f_in ~f_out; + compile opts ~verbosely ~f_in ~f_out; CoqworkmgrApi.giveback 1 -let compile_file (verbosely,f_in) = +let compile_file opts (f_in, verbosely) = if !Flags.beautify then Flags.with_option Flags.beautify_file - (fun f_in -> compile ~verbosely ~f_in ~f_out:None) f_in + (fun f_in -> compile opts ~verbosely ~f_in ~f_out:None) f_in else - compile ~verbosely ~f_in ~f_out:None + compile opts ~verbosely ~f_in ~f_out:None -let compile_files ~time = - if !compile_list == [] then () - else List.iter (compile_file ~time) (List.rev !compile_list) +let compile_files opts = + let compile_list = List.rev opts.compile_list in + List.iter (compile_file opts) compile_list (******************************************************************************) (* VIO Dispatching *) (******************************************************************************) - -let vio_tasks = ref [] -let add_vio_task f = - set_batch_mode (); - Flags.quiet := true; - vio_tasks := f :: !vio_tasks - -let check_vio_tasks () = +let check_vio_tasks opts = let rc = List.fold_left (fun acc t -> Vio_checking.check_vio t && acc) - true (List.rev !vio_tasks) in - if not rc then exit 1 + true (List.rev opts.vio_tasks) in + if not rc then fatal_error Pp.(str "VIO Task Check failed") (* vio files *) -let vio_files = ref [] -let vio_files_j = ref 0 -let vio_checking = ref false -let add_vio_file f = - set_batch_mode (); - Flags.quiet := true; - vio_files := f :: !vio_files - -let set_vio_checking_j opt j = - try vio_files_j := int_of_string j - with Failure _ -> - prerr_endline ("The first argument of " ^ opt ^ " must the number"); - prerr_endline "of concurrent workers to be used (a positive integer)."; - prerr_endline "Makefiles generated by coq_makefile should be called"; - prerr_endline "setting the J variable like in 'make vio2vo J=3'"; - exit 1 - -let schedule_vio () = +let schedule_vio opts = (* We must add update the loadpath here as the scheduling process happens outside of the STM *) - let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in + let iload_path = build_load_path opts in List.iter Mltop.add_coq_path iload_path; - if !vio_checking then - Vio_checking.schedule_vio_checking !vio_files_j !vio_files + if opts.vio_checking then + Vio_checking.schedule_vio_checking opts.vio_files_j opts.vio_files else - Vio_checking.schedule_vio_compilation !vio_files_j !vio_files + Vio_checking.schedule_vio_compilation opts.vio_files_j opts.vio_files (******************************************************************************) -(* UI Options *) +(* Color Options *) (******************************************************************************) -(** Options for proof general *) - -let set_emacs () = - if not (Option.is_empty !toploop) then - user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop"); - Coqloop.print_emacs := true; - Printer.enable_goal_tags_printing := true; - color := `OFF - -(** Options for CoqIDE *) - -let set_ideslave () = - if !Coqloop.print_emacs then user_err Pp.(str "Flags -ideslave and -emacs are incompatible"); - toploop := Some "coqidetop"; - Flags.ide_slave := true +let init_color color_mode = + let has_color = match color_mode with + | `OFF -> false + | `ON -> true + | `AUTO -> + Terminal.has_style Unix.stdout && + Terminal.has_style Unix.stderr && + (* emacs compilation buffer does not support colors by default, + its TERM variable is set to "dumb". *) + try Sys.getenv "TERM" <> "dumb" with Not_found -> false + in + if has_color then begin + let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in + match colors with + | None -> + (** Default colors *) + Topfmt.init_terminal_output ~color:true + | Some "" -> + (** No color output *) + Topfmt.init_terminal_output ~color:false + | Some s -> + (** Overwrite all colors *) + Topfmt.clear_styles (); + Topfmt.parse_color_config s; + Topfmt.init_terminal_output ~color:true + end + else + Topfmt.init_terminal_output ~color:false -(** Options for slaves *) +let toploop_init = ref begin fun opts x -> + let () = init_color opts.color in + let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in + x + end -let set_toploop name = - if !Coqloop.print_emacs then user_err Pp.(str "Flags -toploop and -emacs are incompatible"); - toploop := Some name +let print_style_tags opts = + let () = init_color opts.color in + let tags = Topfmt.dump_tags () in + let iter (t, st) = + let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in + print_string opt + in + let make (t, st) = + let tags = List.map string_of_int (Terminal.repr st) in + (t ^ "=" ^ String.concat ";" tags) + in + let repr = List.map make tags in + let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in + let () = List.iter iter tags in + flush_all () (** GC tweaking *) @@ -490,339 +404,37 @@ let init_gc () = Gc.minor_heap_size = 33554432; (** 4M *) Gc.space_overhead = 120} -(*s Parsing of the command line. - We no longer use [Arg.parse], in order to use share [Usage.print_usage] - between coqtop and coqc. *) - -let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem" - (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned") - -exception NoCoqLib - -let usage batch = - begin - try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) - with NoCoqLib -> usage_no_coqlib () - end; - let lp = Coqinit.toplevel_init_load_path () in - (* Necessary for finding the toplevels below *) - List.iter Mltop.add_coq_path lp; - if batch then Usage.print_usage_coqc () - else begin - Mltop.load_ml_objects_raw_rex - (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$")); - Usage.print_usage_coqtop () - end - -let print_style_tags () = - let () = init_color () in - let tags = Topfmt.dump_tags () in - let iter (t, st) = - let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in - print_string opt - in - let make (t, st) = - let tags = List.map string_of_int (Terminal.repr st) in - (t ^ "=" ^ String.concat ";" tags) - in - let repr = List.map make tags in - let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in - let () = List.iter iter tags in - flush_all () - -let error_missing_arg s = - prerr_endline ("Error: extra argument expected after option "^s); - prerr_endline "See -help for the syntax of supported options"; - exit 1 - -let filter_opts = ref false -let exitcode () = if !filter_opts then 2 else 0 - -let print_where = ref false -let print_config = ref false -let print_tags = ref false - -let get_priority opt s = - try CoqworkmgrApi.priority_of_string s - with Invalid_argument _ -> - prerr_endline ("Error: low/high expected after "^opt); exit 1 - -let get_async_proofs_mode opt = let open Stm.AsyncOpts in function - | "no" | "off" -> APoff - | "yes" | "on" -> APon - | "lazy" -> APonLazy - | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 - -let get_cache opt = function - | "force" -> Some Stm.AsyncOpts.Force - | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 - - -let set_worker_id opt s = - assert (s <> "master"); - Flags.async_proofs_worker_id := s - -let get_bool opt = function - | "yes" | "on" -> true - | "no" | "off" -> false - | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 - -let get_int opt n = - try int_of_string n - with Failure _ -> - prerr_endline ("Error: integer expected after option "^opt); exit 1 - -let get_float opt n = - try float_of_string n - with Failure _ -> - prerr_endline ("Error: float expected after option "^opt); exit 1 - -let get_host_port opt s = - match CString.split ':' s with - | [host; portr; portw] -> - Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) - | ["stdfds"] -> Some Spawned.AnonPipe - | _ -> - prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt); - exit 1 - -let get_error_resilience opt = function - | "on" | "all" | "yes" -> `All - | "off" | "no" -> `None - | s -> `Only (CString.split ',' s) - -let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) - -let is_not_dash_option = function - | Some f when String.length f > 0 && f.[0] <> '-' -> true - | _ -> false - -let get_native_name s = - (* We ignore even critical errors because this mode has to be super silent *) - try - String.concat "/" [Filename.dirname s; - Nativelib.output_dir; Library.native_name_from_filename s] - with _ -> "" - -(** Prints info which is either an error or an anomaly and then exits - with the appropriate error code *) -let fatal_error ?extra exn = - Topfmt.print_err_exn ?extra exn; - let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in - exit exit_code - -let parse_args arglist = - let args = ref arglist in - let extras = ref [] in - let rec parse () = match !args with - | [] -> List.rev !extras - | opt :: rem -> - args := rem; - let next () = match !args with - | x::rem -> args := rem; x - | [] -> error_missing_arg opt - in - let peek_next () = match !args with - | x::_ -> Some x - | [] -> None - in - begin match opt with - - (* Complex options with many args *) - |"-I"|"-include" -> - begin match rem with - | d :: rem -> Coqinit.push_ml_include d; args := rem - | [] -> error_missing_arg opt - end - |"-Q" -> - begin match rem with - | d :: p :: rem -> set_include d p false; args := rem - | _ -> error_missing_arg opt - end - |"-R" -> - begin match rem with - | d :: p :: rem -> set_include d p true; args := rem - | _ -> error_missing_arg opt - end - - (* Options with two arg *) - |"-check-vio-tasks" -> - let tno = get_task_list (next ()) in - let tfile = next () in - add_vio_task (tno,tfile) - |"-schedule-vio-checking" -> - vio_checking := true; - set_vio_checking_j opt (next ()); - add_vio_file (next ()); - while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done - |"-schedule-vio2vo" -> - set_vio_checking_j opt (next ()); - add_vio_file (next ()); - while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done - - (* Options with one arg *) - |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ()) - |"-async-proofs" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next()) - } - |"-async-proofs-j" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ())) - } - |"-async-proofs-cache" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ()) - } - |"-async-proofs-tac-j" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ())) - } - |"-async-proofs-worker-priority" -> - WorkerLoop.async_proofs_worker_priority := get_priority opt (next ()) - |"-async-proofs-private-flags" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_private_flags = Some (next ()); - } - |"-async-proofs-tactic-error-resilience" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ()); - } - |"-async-proofs-command-error-resilience" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ()) - } - |"-async-proofs-delegation-threshold" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ()) - } - |"-worker-id" -> set_worker_id opt (next ()) - |"-compat" -> - let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in - Flags.compat_version := v; add_compat_require v - |"-compile" -> add_compile false (next ()) - |"-compile-verbose" -> add_compile true (next ()) - |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true - |"-feedback-glob" -> Dumpglob.feedback_glob () - |"-exclude-dir" -> System.exclude_directory (next ()) - |"-init-file" -> Coqinit.set_rcfile (next ()) - |"-inputstate"|"-is" -> set_inputstate (next ()) - |"-load-ml-object" -> Mltop.dir_ml_load (next ()) - |"-load-ml-source" -> Mltop.dir_ml_use (next ()) - |"-load-vernac-object" -> add_require (next (), None, None) - |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ()) - |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ()) - |"-outputstate" -> set_outputstate (next ()) - |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 - |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ()) - |"-require" -> add_require (next (), None, Some false) - |"-top" -> set_toplevel_name (dirpath_of_string (next ())) - |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) - |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) - |"-vio2vo" -> - add_compile false (next ()); - compilation_mode := Vio2Vo - |"-toploop" -> set_toploop (next ()) - |"-w" | "-W" -> - let w = next () in - if w = "none" then CWarnings.set_flags w - else - let w = CWarnings.get_flags () ^ "," ^ w in - CWarnings.set_flags (CWarnings.normalize_flags_string w) - |"-o" -> compilation_output_name := Some (next()) - - (* Options with zero arg *) - |"-async-queries-always-delegate" - |"-async-proofs-always-delegate" - |"-async-proofs-full" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_full = true; - } - |"-async-proofs-never-reopen-branch" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_never_reopen_branch = true; - } - |"-batch" -> set_batch_mode () - |"-test-mode" -> Flags.test_mode := true - |"-beautify" -> Flags.beautify := true - |"-boot" -> Flags.boot := true; Coqinit.no_load_rc () - |"-bt" -> Backtrace.record_backtrace true - |"-color" -> set_color (next ()) - |"-config"|"--config" -> print_config := true - |"-debug" -> Coqinit.set_debug () - |"-stm-debug" -> Stm.stm_debug := true - |"-emacs" -> set_emacs () - |"-filteropts" -> filter_opts := true - |"-h"|"-H"|"-?"|"-help"|"--help" -> usage !batch_mode - |"-ideslave" -> set_ideslave () - |"-impredicative-set" -> set_impredicative_set () - |"-indices-matter" -> Indtypes.enforce_indices_matter () - |"-m"|"--memory" -> memory_stat := true - |"-noinit"|"-nois" -> load_init := false - |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true - |"-native-compiler" -> - if not Coq_config.native_compiler then - warning "Native compilation was disabled at configure time." - else Flags.output_native_objects := true - |"-output-context" -> output_context := true - |"-profile-ltac" -> Flags.profile_ltac := true - |"-q" -> Coqinit.no_load_rc () - |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false - |"-quick" -> compilation_mode := BuildVio - |"-list-tags" -> print_tags := true - |"-time" -> measure_time := true - |"-type-in-type" -> set_type_in_type () - |"-unicode" -> add_require ("Utf8_core", None, Some false) - |"-v"|"--version" -> Usage.version (exitcode ()) - |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ()) - |"-where" -> print_where := true - - (* Unknown option *) - | s -> extras := s :: !extras - end; - parse () - in - try - parse () - with any -> fatal_error any - +(** Main init routine *) let init_toplevel arglist = (* Coq's init process, phase 1: - - OCaml parameters, and basic structures and IO + OCaml parameters, basic structures, and IO *) CProfile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) let init_feeder = Feedback.add_feeder coqtop_init_feed in Lib.init(); + (* Coq's init process, phase 2: - - Basic Coq environment, load-path, plugins. + Basic Coq environment, load-path, plugins. *) let res = begin try - let extras = parse_args arglist in + let opts,extras = parse_args arglist in + memory_stat := opts.memory_stat; + (* If we have been spawned by the Spawn module, this has to be done * early since the master waits us to connect back *) Spawned.init_channels (); Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); - if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ())); - if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ())); - if !print_tags then (print_style_tags (); exit (exitcode ())); - if !filter_opts then (print_string (String.concat "\n" extras); exit 0); + if opts.print_where then (print_endline(Envars.coqlib ()); exit(exitcode opts)); + if opts.print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode opts)); + if opts.print_tags then (print_style_tags opts; exit (exitcode opts)); + if opts.filter_opts then (print_string (String.concat "\n" extras); exit 0); let top_lp = Coqinit.toplevel_init_load_path () in List.iter Mltop.add_coq_path top_lp; - Option.iter Mltop.load_ml_object_raw !toploop; - let extras = !toploop_init extras in + Option.iter Mltop.load_ml_object_raw opts.toploop; + let extras = !toploop_init opts extras in if not (CList.is_empty extras) then begin prerr_endline ("Don't know what to do with "^String.concat " " extras); prerr_endline "See -help for the list of supported options"; @@ -830,10 +442,10 @@ let init_toplevel arglist = end; Flags.if_verbose print_header (); Mltop.init_known_plugins (); - engage (); + Global.set_engagement opts.impredicative_set; (* Allow the user to load an arbitrary state here *) - inputstate (); + inputstate opts; (* This state will be shared by all the documents *) Stm.init_core (); @@ -842,9 +454,7 @@ let init_toplevel arglist = It is essential that the module system is in a consistent state before we take the first snapshot. This was not - guaranteed in the past. In particular, we want to be sure we - have called start_library before loading the prelude and rest - of required files. + guaranteed in the past, but now is thanks to the STM API. We split the codepath here depending whether coqtop is called in interactive mode or not. *) @@ -852,39 +462,40 @@ let init_toplevel arglist = (* The condition for starting the interactive mode is a bit convoluted, we should really refactor batch/compilation_mode more. *) - if (not !batch_mode - || CList.(is_empty !compile_list && is_empty !vio_files && is_empty !vio_tasks)) + if (not opts.batch_mode + || CList.(is_empty opts.compile_list && is_empty opts.vio_files && is_empty opts.vio_tasks)) (* Interactive *) then begin - let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in - let require_libs = require_libs () in - let stm_options = !top_stm_options in + let iload_path = build_load_path opts in + let require_libs = require_libs opts in + let stm_options = opts.stm_flags in try - let doc, sid = Stm.(new_doc - { doc_type = Interactive !toplevel_name; - iload_path; - require_libs; - stm_options; - }) in - Some (load_init_vernaculars ~time:!measure_time doc sid) - with any -> flush_all(); fatal_error any - (* Non interactive *) + let open Vernac.State in + let doc, sid = + Stm.(new_doc + { doc_type = Interactive opts.toplevel_name; + iload_path; require_libs; stm_options; + }) in + let state = { doc; sid; proof = None } in + Some (load_init_vernaculars opts ~state), opts + with any -> flush_all(); fatal_error_exn any + (* Non interactive: we perform a sequence of compilation steps *) end else begin try - compile_files ~time:!measure_time; + compile_files opts; (* Vio compile pass *) - if !vio_files <> [] then schedule_vio (); + if opts.vio_files <> [] then schedule_vio opts; (* Vio task pass *) - check_vio_tasks (); + check_vio_tasks opts; (* Allow the user to output an arbitrary state *) - outputstate (); - None - with any -> flush_all(); fatal_error any + outputstate opts; + None, opts + with any -> flush_all(); fatal_error_exn any end; with any -> flush_all(); let extra = Some (str "Error during initialization: ") in - fatal_error ?extra any + fatal_error_exn ?extra any end in Feedback.del_feeder init_feeder; res @@ -892,12 +503,12 @@ let init_toplevel arglist = let start () = match init_toplevel (List.tl (Array.to_list Sys.argv)) with (* Batch mode *) - | Some (doc, sid) when not !batch_mode -> - !toploop_run doc; + | Some state, opts when not opts.batch_mode -> + !toploop_run opts ~state; exit 1 - | _ -> + | _ , opts -> flush_all(); - if !output_context then begin + if opts.output_context then begin let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 5b9494eaa..dedb298e2 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -11,14 +11,13 @@ state, load the files given on the command line, load the resource file, produce the output state if any, and finally will launch [Coqloop.loop]. *) -val init_toplevel : string list -> (Stm.doc * Stateid.t) option +val init_toplevel : string list -> Vernac.State.t option * Coqargs.coq_cmdopts val start : unit -> unit (* Last document seen after `Drop` *) -val drop_last_doc : Stm.doc option ref +val drop_last_doc : Vernac.State.t option ref (* For other toploops *) -val toploop_init : (string list -> string list) ref -val toploop_run : (Stm.doc -> unit) ref - +val toploop_init : (Coqargs.coq_cmdopts -> string list -> string list) ref +val toploop_run : (Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit) ref diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 10bf48647..9fb2e33d7 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -2,4 +2,5 @@ Vernac Usage Coqloop Coqinit +Coqargs Coqtop diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 6b45a94bc..1f681d9cf 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -110,14 +110,25 @@ let pr_open_cur_subgoals () = (* Stm.End_of_input -> true *) (* | _ -> false *) -let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) = +module State = struct + + type t = { + doc : Stm.doc; + sid : Stateid.t; + proof : Proof.t option; + } + +end + +let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = + let open State in let interp v = match under_control v with | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in - load_vernac ~time ~verbosely ~check ~interactive doc sid f + load_vernac ~time ~verbosely ~check ~interactive ~state f | _ -> (* XXX: We need to run this before add as the classification is highly dynamic and depends on the structure of the @@ -134,7 +145,7 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) = in CWarnings.set_flags wflags; - let doc, nsid, ntip = Stm.add ~doc ~ontop:sid (not !Flags.quiet) (loc,v) in + let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,v) in (* Main STM interaction *) if ntip <> `NewTip then @@ -152,7 +163,8 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) = is_proof_step && Proof_global.there_are_pending_proofs () in if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); - ndoc, nsid + let new_proof = Proof_global.give_me_the_proof_opt () in + { doc = ndoc; sid = nsid; proof = new_proof } in try (* The -time option is only supported from console-based @@ -163,7 +175,7 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) = with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) - if interactive then ignore(Stm.edit_at ~doc sid); + if interactive then ignore(Stm.edit_at ~doc:state.doc state.sid); let (reraise, info) = CErrors.push reraise in let info = begin match Loc.get_loc info with @@ -172,7 +184,7 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) = end in iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -and load_vernac ~time ~verbosely ~check ~interactive doc sid file = +and load_vernac ~time ~verbosely ~check ~interactive ~state file = let ft_beautify, close_beautify = if !Flags.beautify_file then let chan_beautify = open_out (file^beautify_suffix) in @@ -183,14 +195,14 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file = let in_chan = open_utf8_file_in file in let in_echo = if verbosely then Some (open_utf8_file_in file) else None in let in_pa = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in - let rsid = ref sid in - let rdoc = ref doc in + let rstate = ref state in + let open State in try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do let loc, ast = - Stm.parse_sentence ~doc:!rdoc !rsid in_pa + Stm.parse_sentence ~doc:!rstate.doc !rstate.sid in_pa (* If an error in parsing occurs, we propagate the exception so the caller of load_vernac will take care of it. However, in the future it could be possible that we want to handle @@ -214,11 +226,10 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file = Option.iter (vernac_echo ?loc) in_echo; checknav_simple (loc, ast); - let ndoc, nsid = Flags.silently (interp_vernac ~time ~check ~interactive !rdoc !rsid) (loc, ast) in - rsid := nsid; - rdoc := ndoc + let state = Flags.silently (interp_vernac ~time ~check ~interactive ~state:!rstate) (loc, ast) in + rstate := state; done; - !rdoc, !rsid + !rstate with any -> (* whatever the exception *) let (e, info) = CErrors.push any in close_in in_chan; @@ -229,7 +240,7 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file = if !Flags.beautify then pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa ft_beautify None; if !Flags.beautify_file then close_beautify (); - !rdoc, !rsid + !rstate | reraise -> if !Flags.beautify_file then close_beautify (); iraise (disable_drop e, info) @@ -241,6 +252,6 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file = of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -let process_expr ~time doc sid loc_ast = +let process_expr ~time ~state loc_ast = checknav_deep loc_ast; - interp_vernac ~time ~interactive:true ~check:true doc sid loc_ast + interp_vernac ~time ~interactive:true ~check:true ~state loc_ast diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index b77b024fa..e909ada1e 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -7,14 +7,24 @@ (************************************************************************) (** Parsing of vernacular. *) +module State : sig + + type t = { + doc : Stm.doc; + sid : Stateid.t; + proof : Proof.t option; + } + +end (** [process_expr sid cmd] Executes vernac command [cmd]. Callers are expected to handle and print errors in form of exceptions, however care is taken so the state machine is left in a consistent state. *) -val process_expr : time:bool -> Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t +val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control Loc.located -> State.t (** [load_vernac echo sid file] Loads [file] on top of [sid], will echo the commands if [echo] is set. Callers are expected to handle and print errors in form of exceptions. *) -val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t +val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool -> + state:State.t -> string -> State.t diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 1bb9e0da1..3be357598 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -606,8 +606,8 @@ let distribute a ll = List.map (fun l -> a @ l) ll t;sep;t;...;t;sep;t;...;t;sep;t;LIST1(t,sep) *) let expand_list_rule typ tkl x n p ll = - let camlp4_message_name = Some (add_suffix x ("_"^string_of_int n)) in - let main = GramConstrNonTerminal (ETConstr typ, camlp4_message_name) in + let camlp5_message_name = Some (add_suffix x ("_"^string_of_int n)) in + let main = GramConstrNonTerminal (ETConstr typ, camlp5_message_name) in let tks = List.map (fun x -> GramConstrTerminal x) tkl in let rec aux i hds ll = if i < p then aux (i+1) (main :: tks @ hds) ll diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index b3049f1b7..e064b570e 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -51,7 +51,7 @@ val add_syntax_extension : val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> bool -> Flags.compat_version option -> unit -(** Print the Camlp4 state of a grammar *) +(** Print the Camlp5 state of a grammar *) val pr_grammar : string -> Pp.t diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 7e96f28de..1ad7ead72 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Feedback open Pp (** Pp control also belongs here as the terminal is private to the toplevel *) @@ -138,7 +137,7 @@ let make_body quoter info ?pre_hdr s = (* The empty quoter *) let noq x = x (* Generic logger *) -let gen_logger dbg warn ?pre_hdr level msg = match level with +let gen_logger dbg warn ?pre_hdr level msg = let open Feedback in match level with | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?pre_hdr msg) | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg) | Notice -> msgnl_with !std_ft (make_body noq info_hdr ?pre_hdr msg) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7223389c4..35ef4bfa4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -58,20 +58,20 @@ let show_proof () = let p = Proof_global.give_me_the_proof () in let sigma, env = Pfedit.get_current_context () in let pprf = Proof.partial_proof p in - Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) + Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in - Feedback.msg_notice (pr_evars_int sigma 1 (Evd.undefined_map sigma)) + pr_evars_int sigma 1 (Evd.undefined_map sigma) let show_universes () = let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in - Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma)); - Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx) + Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ + str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx (* Simulate the Intro(s) tactic *) let show_intro all = @@ -83,11 +83,12 @@ let show_intro all = let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in - Feedback.msg_notice (hov 0 (prlist_with_sep spc Id.print lid)) + hov 0 (prlist_with_sep spc Id.print lid) else if not (List.is_empty l) then let n = List.last l in - Feedback.msg_notice (Id.print (List.hd (Tactics.find_intro_names [n] gl))) - end + Id.print (List.hd (Tactics.find_intro_names [n] gl)) + else mt () + end else mt () (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -146,8 +147,8 @@ let show_match id = let pr_branch l = str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>" in - Feedback.msg_notice (v 1 (str "match # with" ++ fnl () ++ - prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ())) + v 1 (str "match # with" ++ fnl () ++ + prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ()) (* "Print" commands *) @@ -186,21 +187,21 @@ let print_module r = let globdir = Nametab.locate_dir qid in match globdir with DirModule { obj_dir; obj_mp; _ } -> - Feedback.msg_notice (Printmod.print_module (Printmod.printable_body obj_dir) obj_mp) + Printmod.print_module (Printmod.printable_body obj_dir) obj_mp | _ -> raise Not_found with - Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) + Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) let print_modtype r = let (loc,qid) = qualid_of_reference r in try let kn = Nametab.locate_modtype qid in - Feedback.msg_notice (Printmod.print_modtype kn) + Printmod.print_modtype kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try let mp = Nametab.locate_module qid in - Feedback.msg_notice (Printmod.print_module false mp) + Printmod.print_module false mp with Not_found -> user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) @@ -272,7 +273,7 @@ let print_namespace ns = acc ) constants (str"") in - Feedback.msg_notice ((print_list Id.print ns)++str":"++fnl()++constants_in_namespace) + (print_list Id.print ns)++str":"++fnl()++constants_in_namespace let print_strategy r = let open Conv_oracle in @@ -302,7 +303,7 @@ let print_strategy r = else str "Constant strategies" ++ fnl () ++ hov 0 (prlist_with_sep fnl pr_strategy cst_lvl) in - Feedback.msg_notice (var_msg ++ cst_msg) + var_msg ++ cst_msg | Some r -> let r = Smartlocate.smart_global r in let key = match r with @@ -311,7 +312,7 @@ let print_strategy r = | IndRef _ | ConstructRef _ -> user_err Pp.(str "The reference is not unfoldable") in let lvl = get_strategy oracle key in - Feedback.msg_notice (pr_strategy (r, lvl)) + pr_strategy (r, lvl) let dump_universes_gen g s = let output = open_out s in @@ -345,7 +346,7 @@ let dump_universes_gen g s = try UGraph.dump_universes output_constraint g; close (); - Feedback.msg_info (str "Universes written to file \"" ++ str s ++ str "\".") + str "Universes written to file \"" ++ str s ++ str "\"." with reraise -> let reraise = CErrors.push reraise in close (); @@ -360,12 +361,9 @@ let locate_file f = let msg_found_library = function | Library.LibLoaded, fulldir, file -> - Feedback.msg_info (hov 0 - (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ - str file)) + hov 0 (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ str file) | Library.LibInPath, fulldir, file -> - Feedback.msg_info (hov 0 - (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file)) + hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file) let err_unmapped_library ?loc ?from qid = let dir = fst (repr_qualid qid) in @@ -944,7 +942,6 @@ let vernac_chdir = function end; Flags.if_verbose Feedback.msg_info (str (Sys.getcwd())) - (********************) (* State management *) @@ -1595,9 +1592,9 @@ let vernac_check_may_eval ~atts redexp glopt rc = let evars_of_term c = Evarutil.undefined_evars_of_term sigma' c in let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma' j.Environ.uj_type } in - Feedback.msg_notice (print_judgment env sigma' j ++ - pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx_set sigma uctx) + print_judgment env sigma' j ++ + pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ + Printer.pr_universe_ctx_set sigma uctx | Some r -> let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in let redfun env evm c = @@ -1605,7 +1602,7 @@ let vernac_check_may_eval ~atts redexp glopt rc = let (_, c) = redfun env evm c in c in - Feedback.msg_notice (print_eval redfun env sigma' rc j) + print_eval redfun env sigma' rc j let vernac_declare_reduction ~atts s r = let local = make_locality atts.locality in @@ -1621,8 +1618,8 @@ let vernac_global_check c = let senv = Safe_typing.push_context_set false uctx senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in - Feedback.msg_notice (print_safe_judgment env sigma j ++ - pr_universe_ctx_set sigma uctx) + print_safe_judgment env sigma j ++ + pr_universe_ctx_set sigma uctx let get_nth_goal n = @@ -1630,7 +1627,7 @@ let get_nth_goal n = let gls,_,_,_,sigma = Proof.proof pf in let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in gl - + exception NoHyp (* Printing "About" information of a hypothesis of the current goal. We only print the type and a small statement to this comes from the @@ -1664,31 +1661,32 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~atts env sigma = - let open Feedback in let loc = atts.loc in function - | PrintTables -> msg_notice (print_tables ()) - | PrintFullContext-> msg_notice (print_full_context_typ env sigma) - | PrintSectionContext qid -> msg_notice (print_sec_context_typ env sigma qid) - | PrintInspect n -> msg_notice (inspect env sigma n) - | PrintGrammar ent -> msg_notice (Metasyntax.pr_grammar ent) - | PrintLoadPath dir -> (* For compatibility ? *) msg_notice (print_loadpath dir) - | PrintModules -> msg_notice (print_modules ()) + | PrintTables -> print_tables () + | PrintFullContext-> print_full_context_typ env sigma + | PrintSectionContext qid -> print_sec_context_typ env sigma qid + | PrintInspect n -> inspect env sigma n + | PrintGrammar ent -> Metasyntax.pr_grammar ent + | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir + | PrintModules -> print_modules () | PrintModule qid -> print_module qid | PrintModuleType qid -> print_modtype qid | PrintNamespace ns -> print_namespace ns - | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ()) - | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) - | PrintDebugGC -> msg_notice (Mltop.print_gc ()) - | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl) - | PrintGraph -> msg_notice (Prettyp.print_graph env sigma) - | PrintClasses -> msg_notice (Prettyp.print_classes()) - | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) - | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c)) - | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma) + | PrintMLLoadPath -> Mltop.print_ml_path () + | PrintMLModules -> Mltop.print_ml_modules () + | PrintDebugGC -> Mltop.print_gc () + | PrintName (qid,udecl) -> + dump_global qid; + print_name env sigma qid udecl + | PrintGraph -> Prettyp.print_graph env sigma + | PrintClasses -> Prettyp.print_classes() + | PrintTypeClasses -> Prettyp.print_typeclasses() + | PrintInstances c -> Prettyp.print_instances (smart_global c) + | PrintCoercions -> Prettyp.print_coercions env sigma | PrintCoercionPaths (cls,clt) -> - msg_notice (Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt)) - | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma) + Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt) + | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma | PrintUniverses (b, dst) -> let univ = Global.universes () in let univ = if b then UGraph.sort_universes univ else univ in @@ -1697,23 +1695,24 @@ let vernac_print ~atts env sigma = else str"There may remain asynchronous universe constraints" in begin match dst with - | None -> msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) + | None -> UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining | Some s -> dump_universes_gen univ s end - | PrintHint r -> msg_notice (Hints.pr_hint_ref env sigma (smart_global r)) - | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) - | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name env sigma s) - | PrintHintDb -> msg_notice (Hints.pr_searchtable env sigma) + | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r) + | PrintHintGoal -> Hints.pr_applicable_hint () + | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s + | PrintHintDb -> Hints.pr_searchtable env sigma | PrintScopes -> - msg_notice (Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env))) + Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env)) | PrintScope s -> - msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s) + Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s | PrintVisibility s -> - msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s) + Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s | PrintAbout (ref_or_by_not,udecl,glnumopt) -> - msg_notice (print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt) + print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt | PrintImplicit qid -> - dump_global qid; msg_notice (print_impargs qid) + dump_global qid; + print_impargs qid | PrintAssumptions (o,t,r) -> (* Prints all the axioms and section variables used by a term *) let gr = smart_global r in @@ -1721,7 +1720,7 @@ let vernac_print ~atts env sigma = let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in - msg_notice (Printer.pr_assumptionset env sigma nassums) + Printer.pr_assumptionset env sigma nassums | PrintStrategy r -> print_strategy r let global_module r = @@ -1807,19 +1806,18 @@ let vernac_search ~atts s gopt r = | SearchAbout sl -> (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r |> Search.prioritize_search) pr_search -let vernac_locate = let open Feedback in function - | LocateAny (AN qid) -> msg_notice (print_located_qualid qid) - | LocateTerm (AN qid) -> msg_notice (print_located_term qid) +let vernac_locate = function + | LocateAny (AN qid) -> print_located_qualid qid + | LocateTerm (AN qid) -> print_located_term qid | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *) | LocateTerm (ByNotation (_, (ntn, sc))) -> let _, env = Pfedit.get_current_context () in - msg_notice - (Notation.locate_notation - (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc) + Notation.locate_notation + (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc | LocateLibrary qid -> print_located_library qid - | LocateModule qid -> msg_notice (print_located_module qid) - | LocateOther (s, qid) -> msg_notice (print_located_other s qid) - | LocateFile f -> msg_notice (locate_file f) + | LocateModule qid -> print_located_module qid + | LocateOther (s, qid) -> print_located_other s qid + | LocateFile f -> locate_file f let vernac_register id r = if Proof_global.there_are_pending_proofs () then @@ -1851,7 +1849,7 @@ let vernac_unfocus () = let vernac_unfocused () = let p = Proof_global.give_me_the_proof () in if Proof.unfocused p then - Feedback.msg_notice (str"The proof is indeed fully unfocused.") + str"The proof is indeed fully unfocused." else user_err Pp.(str "The proof is not fully unfocused.") @@ -1878,21 +1876,20 @@ let vernac_bullet (bullet : Proof_bullet.t) = Proof_global.simple_with_current_proof (fun _ p -> Proof_bullet.put p bullet) -let vernac_show = let open Feedback in function +let vernac_show = function | ShowScript -> assert false (* Only the stm knows the script *) | ShowGoal goalref -> let proof = Proof_global.give_me_the_proof () in - let info = match goalref with - | OpenSubgoals -> pr_open_subgoals ~proof - | NthGoal n -> pr_nth_open_subgoal ~proof n - | GoalId id -> pr_goal_by_id ~proof id - in - msg_notice info + begin match goalref with + | OpenSubgoals -> pr_open_subgoals ~proof + | NthGoal n -> pr_nth_open_subgoal ~proof n + | GoalId id -> pr_goal_by_id ~proof id + end | ShowProof -> show_proof () | ShowExistentials -> show_top_evars () | ShowUniverses -> show_universes () | ShowProofNames -> - msg_notice (pr_sequence Id.print (Proof_global.get_all_proof_names())) + pr_sequence Id.print (Proof_global.get_all_proof_names()) | ShowIntros all -> show_intro all | ShowMatch id -> show_match id @@ -1907,8 +1904,7 @@ let vernac_check_guard () = (str "The condition holds up to here") with UserError(_,s) -> (str ("Condition violated: ") ++s) - in - Feedback.msg_notice message + in message exception End_of_input @@ -2063,26 +2059,32 @@ let interp ?proof ~atts ~st c = | VernacAddOption (key,v) -> vernac_add_option key v | VernacMemOption (key,v) -> vernac_mem_option key v | VernacPrintOption key -> vernac_print_option key - | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ~atts r g c + | VernacCheckMayEval (r,g,c) -> + Feedback.msg_notice @@ vernac_check_may_eval ~atts r g c | VernacDeclareReduction (s,r) -> vernac_declare_reduction ~atts s r - | VernacGlobalCheck c -> vernac_global_check c + | VernacGlobalCheck c -> + Feedback.msg_notice @@ vernac_global_check c | VernacPrint p -> let sigma, env = Pfedit.get_current_context () in - vernac_print ~atts env sigma p + Feedback.msg_notice @@ vernac_print ~atts env sigma p | VernacSearch (s,g,r) -> vernac_search ~atts s g r - | VernacLocate l -> vernac_locate l + | VernacLocate l -> + Feedback.msg_notice @@ vernac_locate l | VernacRegister (id, r) -> vernac_register id r | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n") (* Proof management *) | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () - | VernacUnfocused -> vernac_unfocused () + | VernacUnfocused -> + Feedback.msg_notice @@ vernac_unfocused () | VernacBullet b -> vernac_bullet b | VernacSubproof n -> vernac_subproof n | VernacEndSubproof -> vernac_end_subproof () - | VernacShow s -> vernac_show s - | VernacCheckGuard -> vernac_check_guard () + | VernacShow s -> + Feedback.msg_notice @@ vernac_show s + | VernacCheckGuard -> + Feedback.msg_notice @@ vernac_check_guard () | VernacProof (tac, using) -> let using = Option.append using (Proof_using.get_default_proof_using ()) in let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in @@ -2277,8 +2279,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = then Flags.verbosely control c else control c -(* XXX: There is a bug here in case of an exception, see @gares - comments on the PR *) +(* Be careful with the cache here in case of an exception. *) let interp ?verbosely ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; try |