diff options
94 files changed, 798 insertions, 470 deletions
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index c7437c4a4..a9230042a 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -13,4 +13,4 @@ Fixes / closes #???? <!-- If this is a feature pull request / breaks compatibility: --> <!-- (Otherwise, remove these lines.) --> - [ ] Corresponding documentation was added / updated. -- [ ] Entry added in [CHANGES](/CHANGES). +- [ ] Entry added in CHANGES. diff --git a/.gitignore b/.gitignore index 27ac0631a..1e7f982a5 100644 --- a/.gitignore +++ b/.gitignore @@ -85,6 +85,7 @@ test-suite/coq-makefile/merlin1/.merlin test-suite/coqdoc/Coqdoc.* test-suite/coqdoc/index.html test-suite/coqdoc/coqdoc.css +test-suite/output/MExtraction.out # documentation diff --git a/.travis.yml b/.travis.yml index 0bc43c110..8f1f1e699 100644 --- a/.travis.yml +++ b/.travis.yml @@ -35,7 +35,7 @@ env: - CAMLP5_VER_BE="7.03" - FINDLIB_VER="1.4.1" - FINDLIB_VER_BE="1.7.3" - - LABLGTK="lablgtk.2.16.0 lablgtk-extras.1.5" + - LABLGTK="lablgtk.2.18.3 lablgtk-extras.1.6" - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6" - NATIVE_COMP="yes" - COQ_DEST="-local" @@ -37,6 +37,9 @@ Tactics - Added tactics reset ltac profile, show ltac profile (and variants) - Added tactics restart_timer, finish_timing, and time_constr as an experimental way of timing Ltac's evaluation phase +- Added tactic optimize_heap, analogous to the Vernacular Optimize + Heap, which performs a major garbage collection and heap compaction + in the OCaml run-time system. Focusing diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 37b556c55..1a769333c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -28,6 +28,8 @@ Please make pull requests against the `master` branch. It's helpful to run the Coq test suite with `make test-suite` before submitting your change. Travis CI runs this test suite and a much larger one including external Coq developments on every pull request, but these results take significantly longer to come back (on the order of a few hours). Running the test suite locally will take somewhere around 10-15 minutes. Refer to [`dev/ci/README.md`](/dev/ci/README.md#information-for-developers) for more information on Travis CI tests. +If your pull request fixes a bug, please consider adding a regression test as well. See [`test-suite/README.md`](/test-suite/README.md) for how to do so. + Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes. Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests. diff --git a/INSTALL.ide b/INSTALL.ide index 513e37c91..26c192baa 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -39,7 +39,7 @@ COMPILATION REQUIREMENTS install GTK+ 2.x, should you need to force it for one reason or another.) - The OCaml bindings for GTK+ 2.x, lablgtk2 with support for gtksourceview2. - You need at least version 2.16. + You need at least version 2.18.3. Your distribution may contain precompiled packages. For example, for Debian, run @@ -57,7 +57,7 @@ COMPILATION REQUIREMENTS ./configure && make world && make install You must have write access to the OCaml standard library path. - If this fails, read lablgtk-2.14.2/README. + If this fails, read the README. INSTALLATION @@ -43,8 +43,8 @@ package "lib" ( requires = "coq.clib, coq.config" - archive(byte) += "lib.cma" - archive(native) += "lib.cmxa" + archive(byte) = "lib.cma" + archive(native) = "lib.cmxa" ) diff --git a/Makefile.build b/Makefile.build index 9a838b85c..d8474ae13 100644 --- a/Makefile.build +++ b/Makefile.build @@ -600,10 +600,26 @@ COND_BYTEFLAGS= \ COND_OPTFLAGS= \ $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(OPTFLAGS) +plugins/micromega/%.cmi: plugins/micromega/%.mli + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< + +plugins/nsatz/%.cmi: plugins/nsatz/%.mli + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< + %.cmi: %.mli $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< +plugins/micromega/%.cmo: plugins/micromega/%.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< + +plugins/nsatz/%.cmo: plugins/nsatz/%.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< + %.cmo: %.ml $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< @@ -637,6 +653,14 @@ plugins/micromega/sos_FORPACK:= plugins/micromega/sos_print_FORPACK:= plugins/micromega/csdpcert_FORPACK:= +plugins/micromega/%.cmx: plugins/micromega/%.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $< + +plugins/nsatz/%.cmx: plugins/nsatz/%.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $< + plugins/%.cmx: plugins/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $< diff --git a/Makefile.checker b/Makefile.checker index 5b5855782..8334b6a2a 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -33,7 +33,7 @@ CHECKERDEPS := $(addsuffix .d, $(CHECKMLDFILE) $(CHECKMLLIBFILE)) -include $(CHECKERDEPS) ifeq ($(BEST),opt) -$(CHICKEN): checker/check.cmxa checker/main.ml +$(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^ $(STRIP) $@ @@ -43,7 +43,7 @@ $(CHICKEN): $(CHICKENBYTE) cp $< $@ endif -$(CHICKENBYTE): checker/check.cma checker/main.ml +$(CHICKENBYTE): checker/check.cma checker/main.mli checker/main.ml $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^ diff --git a/Makefile.ide b/Makefile.ide index 08829b554..09eef1f6b 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -45,8 +45,8 @@ IDEDEPS:=clib/clib.cma lib/lib.cma IDECMA:=ide/ide.cma IDETOPLOOPCMA=ide/coqidetop.cma -LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml +LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.mli ide/coqide_main.ml +LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.mli ide/coqide_main.ml IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map diff --git a/checker/checker.mli b/checker/checker.mli new file mode 100644 index 000000000..ceab13774 --- /dev/null +++ b/checker/checker.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val start : unit -> unit diff --git a/checker/main.mli b/checker/main.mli new file mode 100644 index 000000000..e1555ba2e --- /dev/null +++ b/checker/main.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This empty file avoids a race condition that occurs when compiling a .ml file + that does not have a corresponding .mli file *) diff --git a/checker/print.mli b/checker/print.mli new file mode 100644 index 000000000..3b2715de9 --- /dev/null +++ b/checker/print.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Cic + +val print_pure_constr : constr -> unit diff --git a/checker/univ.ml b/checker/univ.ml index 4f3131813..7d01657df 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -881,14 +881,6 @@ type universe_level_subst = universe_level universe_map (** A full substitution might involve algebraic universes *) type universe_subst = universe universe_map -let level_subst_of f = - fun l -> - try let u = f l in - match Universe.level u with - | None -> l - | Some l -> l - with Not_found -> l - module Instance : sig type t = Level.t array diff --git a/checker/univ.mli b/checker/univ.mli index 0eadc6801..21c94d952 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -150,8 +150,6 @@ type universe_level_subst_fn = universe_level -> universe_level type universe_subst = universe universe_map type universe_level_subst = universe_level universe_map -val level_subst_of : universe_subst_fn -> universe_level_subst_fn - (** {6 Universe instances} *) module Instance : diff --git a/checker/validate.ml b/checker/validate.ml index 820040587..2624e6d49 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -49,8 +49,6 @@ let (/) (ctx:error_context) s : error_context = s::ctx exception ValidObjError of string * error_context * Obj.t let fail ctx o s = raise (ValidObjError(s,ctx,o)) -type func = error_context -> Obj.t -> unit - (* Check that object o is a block with tag t *) let val_tag t ctx o = if Obj.is_block o && Obj.tag o = t then () diff --git a/checker/validate.mli b/checker/validate.mli new file mode 100644 index 000000000..7eed692a0 --- /dev/null +++ b/checker/validate.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val validate : bool -> Values.value -> 'a -> unit diff --git a/checker/values.ml b/checker/values.ml index 5a371164c..4698227ff 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -372,22 +372,3 @@ let v_lib = let v_opaques = Array (v_computation v_constr) let v_univopaques = Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|])) - -(** Registering dynamic values *) - -module IntOrd = -struct - type t = int - let compare (x : t) (y : t) = compare x y -end - -module IntMap = Map.Make(IntOrd) - -let dyn_table : value IntMap.t ref = ref IntMap.empty - -let register_dyn name t = - dyn_table := IntMap.add name t !dyn_table - -let find_dyn name = - try IntMap.find name !dyn_table - with Not_found -> Any diff --git a/checker/values.mli b/checker/values.mli new file mode 100644 index 000000000..aad8fd5f4 --- /dev/null +++ b/checker/values.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type value = + | Any + | Fail of string + | Tuple of string * value array + | Sum of string * int * value array array + | Array of value + | List of value + | Opt of value + | Int + | String + | Annot of string * value + | Dyn + +val v_univopaques : value +val v_libsum : value +val v_lib : value +val v_opaques : value +val v_stm_seg : value diff --git a/checker/votour.ml b/checker/votour.ml index 77c9999c4..8cb97a2b1 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -210,7 +210,6 @@ let access_list v o pos = let access_block o = match Repr.repr o with | BLOCK (tag, os) -> (tag, os) | _ -> raise Exit -let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit (** raises Exit if the object has not the expected structure *) exception Forbidden @@ -249,8 +248,7 @@ let rec get_children v o pos = match v with |Dyn -> begin match Repr.repr o with | BLOCK (0, [|id; o|]) -> - let n = access_int id in - let tpe = find_dyn n in + let tpe = Any in [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|] | _ -> raise Exit end @@ -395,7 +393,7 @@ let visit_vo f = | None -> () done -let main = +let () = if not !Sys.interactive then Arg.parse [] visit_vo ("votour: guided tour of a Coq .vo or .vi file\n"^ diff --git a/checker/votour.mli b/checker/votour.mli new file mode 100644 index 000000000..e1555ba2e --- /dev/null +++ b/checker/votour.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This empty file avoids a race condition that occurs when compiling a .ml file + that does not have a corresponding .mli file *) diff --git a/configure.ml b/configure.ml index a86b78ba5..e991eadac 100644 --- a/configure.ml +++ b/configure.ml @@ -758,24 +758,20 @@ let get_lablgtkdir () = let check_lablgtk_version src dir = match src with | Manual | Stdlib -> - let test accu f = - if accu then - let test = sprintf "grep -q -w %s %S/glib.mli" f dir in - Sys.command test = 0 - else false - in - let heuristics = [ - "convert_with_fallback"; - "wrap_poll_func"; (** Introduced in lablgtk 2.16 *) - ] in - let ans = List.fold_left test true heuristics in - if ans then printf "Warning: could not check the version of lablgtk2.\n"; - (ans, "an unknown version") + printf "Warning: could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.\n"; + (true, "an unknown version") | OCamlFind -> let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in try let vi = List.map s2i (numeric_prefix_list v) in - ([2; 16] <= vi, v) + if vi = [2; 18; 0] then + begin + (* Version 2.18.3 is known to report incorrectly as 2.18.0 *) + printf "Warning: could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.\n"; + (true, "an unknown version") + end + else + ([2; 18; 3] <= vi, v) with _ -> (false, v) let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native" @@ -802,7 +798,7 @@ let check_coqide () = if dir = "" then set_ide No "LablGtk2 not found"; let (ok, version) = check_lablgtk_version via dir in let found = sprintf "LablGtk2 found (%s, %s)" (get_source via) version in - if not ok then set_ide No (found^", but too old (required >= 2.16, found " ^ version ^ ")"); + if not ok then set_ide No (found^", but too old (required >= 2.18.3, found " ^ version ^ ")"); (* We're now sure to produce at least one kind of coqide *) lablgtkdir := shorten_camllib dir; if !Prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested"); @@ -1056,7 +1052,7 @@ let _ = print_summary () let write_dbg_wrapper f = safe_remove f; - let o = open_out f in + let o = open_out_bin f in (* _bin to avoid adding \r on Cygwin/Windows *) let pr s = fprintf o s in pr "#!/bin/sh\n\n"; pr "###### ocamldebug-coq : a wrapper around ocamldebug for Coq ######\n\n"; diff --git a/default.nix b/default.nix index 3dd24bac4..af2a13a84 100644 --- a/default.nix +++ b/default.nix @@ -36,6 +36,7 @@ stdenv.mkDerivation rec { ocaml findlib camlp5_strict + num ]) ++ (if buildIde then [ diff --git a/dev/README b/dev/README index b446c3e97..6b83579de 100644 --- a/dev/README +++ b/dev/README @@ -1,4 +1,4 @@ -This directory contains informations and tools to help developing the +This directory contains information and tools to help develop the Coq system ====================== @@ -6,30 +6,30 @@ This directory contains informations and tools to help developing the Debugging and profiling (in current directory - see doc/debugging.txt) ----------------------- -ocamldebug-coq: to launch ocaml debugger +ocamldebug-coq: to launch ocaml debugger (generated by the configure script) -db: to install pretty-printers from ocaml debugger -base_db: to install raw pretty-printers from ocaml debugger +db: to install pretty-printers from ocaml debugger +base_db: to install raw pretty-printers from ocaml debugger -include: to install pretty-printers from ocaml toplevel +include: to install pretty-printers from ocaml toplevel (use with the coq Drop command) base_include: to install raw pretty-printers from ocaml toplevel -vm_printers.ml, dev_printers.ml: ML pretty-printers for debugging +vm_printers.ml, top_printers.ml: ML pretty-printers for debugging -Miscellaneous informations about the code (directory doc) +Miscellaneous information about the code (directory doc) ----------------------------------------- -changes.txt: (partial) per-version summary of the evolutions of Coq ML source -style.txt: a few style recommendations for writing Coq ML files -debugging.txt: help for debugging or profiling -universes.txt: help to debug universes -translate.txt: help to use coq translator +changes.md: (partial) per-version summary of the evolution of Coq ML source +style.txt: a few style recommendations for writing Coq ML files +debugging.md: help for debugging or profiling +universes.txt: help for debugging universes +translate.txt: help for using coq translator extensions.txt: some help about TACTIC EXTEND -header: standard header for Coq ML files -perf-analysis: analysis of perfs measured on the compilation of user contribs -cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation +header: standard header for Coq ML files +perf-analysis: analysis of perfs measured on the compilation of user contribs +cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh index cfcc09b32..dc33838f1 100755 --- a/dev/build/osx/make-macos-dmg.sh +++ b/dev/build/osx/make-macos-dmg.sh @@ -25,4 +25,4 @@ mkdir -p _build # Temporary countermeasure to hdiutil error 5341 # head -c9703424 /dev/urandom > $DMGDIR/.padding -hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO _build/CoqIDE_$VERSION.dmg +hdiutil create -imagekey zlib-level=9 -volname coq-$VERSION-installer-macos -srcfolder $DMGDIR -ov -format UDZO _build/coq-$VERSION-installer-macos.dmg diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi index 48f1d3759..2c2f0fa47 100644 --- a/dev/build/windows/patches_coq/coq_new.nsi +++ b/dev/build/windows/patches_coq/coq_new.nsi @@ -15,7 +15,7 @@ SetCompressor lzma !define MY_PRODUCT "Coq" ;Define your own software name here -!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe" +!define OUTFILE "coq-${VERSION}-installer-windows-${ARCH}.exe" !include "MUI2.nsh" !include "FileAssociation.nsh" diff --git a/dev/ci/README.md b/dev/ci/README.md index f4423558c..bb13587e9 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -103,6 +103,8 @@ The process to merge your PR is then to submit PRs to the external development repositories, merge the latter first (if the fixes are backward-compatible), drop the overlay commit and merge the PR on Coq then. +See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. + Travis specific information --------------------------- diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index 72ee89962..dec6f0d18 100644 --- a/dev/ci/appveyor.bat +++ b/dev/ci/appveyor.bat @@ -25,7 +25,7 @@ if %USEOPAM% == false ( -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ -setup %CYGROOT%\%SETUP% || GOTO ErrorExit copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit - 7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit + 7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit ) if %USEOPAM% == true ( diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh new file mode 100644 index 000000000..78789a6fc --- /dev/null +++ b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then + HoTT_CI_BRANCH=check-poly-effects + HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git +fi diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index fa145d498..fd3cbd1bc 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -22,8 +22,8 @@ Debugging from Coq toplevel using Caml trace mechanism printers too. -Debugging from Caml debugger -============================ +Debugging with ocamldebug from Emacs +==================================== Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\ Coq must be configured with `-local` (`./configure -local`) and the @@ -59,6 +59,29 @@ Debugging from Caml debugger from the debugger. If this happens, unset the variable, re-start Emacs, and run the debugger again. +Debugging with ocamldebug from the command line +=============================================== + +In the `coq` directory: +1. (on Cygwin/Windows) Pass the `-no-custom` option to the `configure` script before building Coq. +2. Run `make` (to compile the .v files) +3. Run `make byte` +4. (on Cygwin/Windows) Add the full pathname of the directory `.../kernel/byterun` to your bash PATH. + Alternatively, copy the file `kernel/byterun/dllcoqrun.dll` to a directory that is in the PATH. (The + CAML_LD_LIBRARY_PATH mechanism described at the end of INSTALL isn't working.) +5. Run `dev/ocamldebug-coq bin/coqtop.byte` (on Cygwin/Windows, use `... bin/coqtop.byte.exe`) +6. Enter `source db` to load printers +7. Enter `set arguments -coqlib .` so Coq can find plugins, theories, etc. +8. See the ocamldebug manual for more information. A few points: + - use `break @ Printer 501` to set a breakpoint on line 501 in the Printer module (printer.ml). + `break` can be abbreviated as `b`. + - `backtrace` or `bt` to see the call stack + - `step` or `s` goes into called functions; `next` or `n` skips over them + - `list` or `li` shows the code just before and after the current stack frame + - `print <var>` or `p <var>` to see the value of a variable +Note that `make byte` doesn't recompile .v files. `make` recompiles all of them if there +are changes in any .ml file--safer but much slower. + Global gprof-based profiling ============================ diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi index 80da84517..f48013cf2 100755 --- a/dev/nsis/coq.nsi +++ b/dev/nsis/coq.nsi @@ -13,7 +13,7 @@ SetCompressor lzma !define MY_PRODUCT "Coq" ;Define your own software name here !define COQ_SRC_PATH "..\.." -!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe" +!define OUTFILE "coq-${VERSION}-installer-windows-${ARCH}.exe" !include "MUI2.nsh" !include "FileAssociation.nsh" diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index 4c4dbe1e9..d7acf01f1 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -1,10 +1,11 @@ #!/usr/bin/env bash -# Usage: dev/tools/backport-pr.sh <PR number> +# Usage: dev/tools/backport-pr.sh <PR number> [--stop-before-merging] set -e PRNUM=$1 +OPTION=$2 if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then echo "PR #${PRNUM} does not exist." @@ -49,6 +50,10 @@ else fi +if [[ "${OPTION}" == "--stop-before-merging" ]]; then + exit 0 +fi + git merge -S --no-ff ${BRANCH} -m "${MESSAGE}" git branch -d ${BRANCH} diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py new file mode 100755 index 000000000..beb26d910 --- /dev/null +++ b/dev/tools/github-check-prs.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python3 + +# Requires PyGithub https://pypi.python.org/pypi/PyGithub, for instance +# debian package: python3-github +# nix: nix-shell -p python3 python3Packages.PyGithub --run ./github-check-rebase.py +from github import Github +import argparse + +REPO = "coq/coq" +REBASE_LABEL="needs: rebase" + +parser = argparse.ArgumentParser() +parser.add_argument("--token-file", type=argparse.FileType('r')) +args = parser.parse_args() + +if args.token_file is None: + token = input("Github access token: ").strip() +else: + token = args.token_file.read().rstrip("\n") + args.token_file.close() + +if token == "": + print ("Warning: using the GitHub API without a token") + print ("We may run into rate limit issues") + g = Github() +else: + g = Github(token) + +repo = g.get_repo(REPO) + +for pull in repo.get_pulls(): + # if conflicts then dirty + # otherwise blocked (because I have no rights) + dirty = pull.mergeable_state == "dirty" + labelled = False + for label in repo.get_issue(pull.number).get_labels(): + if label.name == REBASE_LABEL: + labelled = True + if labelled and not dirty: + print ("PR #" + str(pull.number) + " is not dirty but is labelled") + print ("("+ pull.html_url +")") + elif dirty and not labelled: + print ("PR #" + str(pull.number) + " is dirty and not labelled") + print ("("+ pull.html_url +")") + else: + # give some feedback so the user can see we didn't crash + print ("PR #" + str(pull.number) + " OK") diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index 30039d489..8f9d876cb 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -1,4 +1,4 @@ -\achapter{Asynchronous and Parallel Proof Processing} +\achapter{Asynchronous and Parallel Proof Processing\label{Asyncprocessing}} %HEVEA\cutname{async-proofs.html} \aauthor{Enrico Tassi} diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index 436099e74..2d9853430 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -44,9 +44,10 @@ bottom is the status bar. In the script window, you may open arbitrarily many buffers to edit. The \emph{File} menu allows you to open files or create some, save them, print or export them into various formats. Among all these -buffers, there is always one which is the current \emph{running - buffer}, whose name is displayed on a green background, which is the -one where Coq commands are currently executed. +buffers, there is always one which is the current +\emph{running buffer}, whose name is displayed on a background in the +\emph{processed} color (green by default), which is the one where Coq commands +are currently executed. Buffers may be edited as in any text editor, and classical basic editing commands (Copy/Paste, \ldots) are available in the \emph{Edit} @@ -58,12 +59,13 @@ menu. \section{Interactive navigation into \Coq{} scripts} The running buffer is the one where navigation takes place. The -toolbar proposes five basic commands for this. The first one, +toolbar offers five basic navigation commands. The first one, represented by a down arrow icon, is for going forward executing one command. If that command is successful, the part of the script that -has been executed is displayed on a green background. If that command -fails, the error message is displayed in the message window, and the -location of the error is emphasized by a red underline. +has been executed is displayed on a background with the +processed color. If that command fails, the error message is +displayed in the message window, and the location of the error is +emphasized by an underline in the error foreground color (red by default). On Figure~\ref{fig:coqide}, the running buffer is \verb|Fermat.v|, all commands until the \verb|Theorem| have been already executed, and the @@ -71,23 +73,41 @@ user tried to go forward executing \verb|Induction n|. That command failed because no such tactic exist (tactics are now in lowercase\ldots), and the wrong word is underlined. -Notice that the green part of the running buffer is not editable. If +Notice that the processed part of the running buffer is not editable. If you ever want to modify something you have to go backward using the up arrow tool, or even better, put the cursor where you want to go back and use the \textsf{goto} button. Unlike with \verb|coqtop|, you should never use \verb|Undo| to go backward. -Two additional tool buttons exist, one to go directly to the end and -one to go back to the beginning. If you try to go to the end, or in -general to run several commands using the \textsf{goto} button, the - execution will stop whenever an error is found. +There are two additional buttons for navigation within the running buffer. +The ``down'' button with a line goes directly to the end; the ``up'' button +with a line goes back to the beginning. The handling of errors when using the +go-to-the-end button depends on whether \Coq{} is running in asynchronous mode or not +(see Chapter~\ref{Asyncprocessing}). If it is not running in that mode, execution stops +as soon as an error is found. Otherwise, execution continues, and the +error is marked with an underline in the error foreground color, with a background in +the error background color (pink by default). The same characterization of +error-handling applies when running several commands using the \textsf{goto} button. If you ever try to execute a command which happens to run during a long time, and would like to abort it before its termination, you may use the interrupt button (the white cross on a red circle). -Finally, notice that these navigation buttons are also available in -the menu, where their keyboard shortcuts are given. +There are other buttons on the \CoqIDE{} toolbar: a button to save the running +buffer; a button to close the current buffer (an ``X''); buttons to switch among +buffers (left and right arrows); an ``information'' button; and a ``gears'' button. + +The ``information'' button is described in Section~\ref{sec:trytactics}. + +The ``gears'' button submits proof terms to the \Coq{} kernel for type-checking. +When \Coq{} uses asynchronous processing (see Chapter~\ref{Asyncprocessing}), proofs may +have been completed without kernel-checking of generated proof terms. The presence of +unchecked proof terms is indicated by \texttt{Qed} statements +that have a subdued \emph{being-processed} color (light blue by default), +rather than the processed color, though their preceding proofs have the processed color. + +Notice that for all these buttons, except for the ``gears'' button, their operations +are also available in the menu, where their keyboard shortcuts are given. \section[Try tactics automatically]{Try tactics automatically\label{sec:trytactics}} @@ -96,8 +116,8 @@ trying to solve the current goal using simple tactics. If such a tactic succeeds in solving the goal, then its text is automatically inserted into the script. There is finally a combination of these tactics, called the \emph{proof wizard} which will try each of them in -turn. This wizard is also available as a tool button (the light -bulb). The set of tactics tried by the wizard is customizable in +turn. This wizard is also available as a tool button (the ``information'' +button). The set of tactics tried by the wizard is customizable in the preferences. These tactics are general ones, in particular they do not refer to @@ -132,7 +152,7 @@ arguments. \begin{figure}[t] \begin{center} -%HEVEA\imgsrc[alt="coqide query window"]{coqide-queries.png} +%HEVEA\imgsrc[alt="coqide query"]{coqide-queries.png} %BEGIN LATEX \ifpdf % si on est en pdflatex \includegraphics[width=1.0\textwidth]{coqide-queries.png} @@ -141,27 +161,21 @@ arguments. \fi %END LATEX \end{center} -\caption{\CoqIDE{}: the query window} -\label{fig:querywindow} +\caption{\CoqIDE{}: a Print query on a selected phrase} +\label{fig:queryselected} \end{figure} - -We call \emph{query} any vernacular command that do not change the -current state, such as \verb|Check|, \verb|Search|, etc. Those -commands are of course useless during compilation of a file, hence -should not be included in scripts. To run such commands without -writing them in the script, \CoqIDE{} offers another input window -called the \emph{query window}. This window can be displayed on -demand, either by using the \texttt{Window} menu, or directly using -shortcuts given in the \texttt{Queries} menu. Indeed, with \CoqIDE{} -the simplest way to perform a \texttt{Search} on some identifier -is to select it using the mouse, and pressing \verb|F2|. This will -both make appear the query window and run the \texttt{Search} in -it, displaying the result. Shortcuts \verb|F3| and \verb|F4| are for -\verb|Check| and \verb|Print| respectively. -Figure~\ref{fig:querywindow} displays the query window after selection -of the word ``mult'' in the script windows, and pressing \verb|F4| to -print its definition. +We call \emph{query} any vernacular command that does not change the +current state, such as \verb|Check|, \verb|Search|, etc. +To run such commands interactively, without writing them in scripts, +\CoqIDE{} offers a \emph{query pane}. +The query pane can be displayed on demand by using the \texttt{View} menu, +or using the shortcut \verb|F1|. Queries can also be performed by +selecting a particular phrase, then choosing an item from the +\texttt{Queries} menu. The response then appears in the message window. +Figure~\ref{fig:queryselected} shows the result after selecting +of the phrase \verb|Nat.mul| in the script window, and choosing \verb|Print| +from the \texttt{Queries} menu. \section{Compilation} diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index ef0f4af8f..c4c0435c5 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1426,6 +1426,16 @@ You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, whi Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs. +\subsection[Run-time optimization tactic]{Run-time optimization tactic\label{tactic-optimizeheap}}. + +The following tactic behaves like {\tt idtac}, and running it compacts the heap in the +OCaml run-time system. It is analogous to the Vernacular command {\tt Optimize Heap} (see~\ref{vernac-optimizeheap}). + +\tacindex{optimize\_heap} +\begin{quote} +{\tt optimize\_heap}. +\end{quote} + \endinput \subsection{Permutation on closed lists} diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 991c9745e..05775bfbe 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -499,7 +499,7 @@ Claude Marché coordinated the edition of the Reference Manual for Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the extraction tool and module system of {\Coq}. -Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin ando +Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other contributors from Sophia-Antipolis and Nijmegen participated to the extension of the library. @@ -659,7 +659,7 @@ Matthieu Sozeau extended the \textsc{Russell} language, ending in an convenient way to write programs of given specifications, Pierre Corbineau extended the Mathematical Proof Language and the automatization tools that accompany it, Pierre Letouzey supervised and -extended various parts the standard library, Stéphane Glondu +extended various parts of the standard library, Stéphane Glondu contributed a few tactics and improvements, Jean-Marc Notin provided help in debugging, general maintenance and {\tt coqdoc} support, Vincent Siles contributed extensions of the {\tt Scheme} command and @@ -680,7 +680,7 @@ Nicolas Tabareau made the adaptation of the interface of the old the interaction between Coq and its external interfaces. With Samuel Mimram, he also helped making Coq compatible with recent software tools. Russell O'Connor, Cezary Kaliscyk, Milad Niqui contributed to -improved the libraries of integers, rational, and real numbers. We +improve the libraries of integers, rational, and real numbers. We also thank many users and partners for suggestions and feedback, in particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle team, Georges Gonthier and the INRIA-Microsoft Mathematical Components team, @@ -714,7 +714,7 @@ implementation of $\mathbb{N}$, $\mathbb{Z}$ or $\mathbb{Z}/n\mathbb{Z}$. The main other evolutions of the library are due to Hugo Herbelin who -made a revision of the sorting library (includingh a certified +made a revision of the sorting library (including a certified merge-sort) and to Guillaume Melquiond who slightly revised and cleaned up the library of reals. @@ -723,7 +723,7 @@ some efficiency issues and a more flexible construction of module types, Élie Soubiran brought a new model of name equivalence, the $\Delta$-equivalence, which respects as much as possible the names given by the users. He also designed with Pierre Letouzey a new -convenient operator \verb!<+! for nesting functor application, what +convenient operator \verb!<+! for nesting functor application, that provides a light notation for inheriting the properties of cascading modules. diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 2bd50daf3..6b24fdde7 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -564,12 +564,12 @@ used to force Coq to optimize some of its internal data structures. This command forces Coq to shrink the data structure used to represent the ongoing proof. -\subsection[\tt Optimize Heap.]{\tt Optimize Heap.} +\subsection[\tt Optimize Heap.]{\tt Optimize Heap.\label{vernac-optimizeheap}} This command forces the OCaml runtime to perform a heap compaction. -This is in general an expensive operation. See: - \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact} - +This is in general an expensive operation. See: \\ +\ \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact} \\ +There is also an analogous tactic {\tt optimize\_heap} (see~\ref{tactic-optimizeheap}). %%% Local Variables: %%% mode: latex diff --git a/doc/refman/coqide-queries.png b/doc/refman/coqide-queries.png Binary files differindex dea5626f8..7a46ac4e6 100644 --- a/doc/refman/coqide-queries.png +++ b/doc/refman/coqide-queries.png diff --git a/doc/refman/coqide.png b/doc/refman/coqide.png Binary files differindex a6a0f5850..e300401c9 100644 --- a/doc/refman/coqide.png +++ b/doc/refman/coqide.png diff --git a/engine/evd.ml b/engine/evd.ml index e33c851f6..0e9472158 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -855,7 +855,7 @@ let normalize_universe evd = let normalize_universe_instance evd l = let vars = ref (UState.subst evd.universes) in - let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in + let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l let normalize_sort evars s = diff --git a/engine/uState.ml b/engine/uState.ml index 6131f4c03..6f2b3c4b2 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -516,7 +516,7 @@ let is_sort_variable uctx s = | _ -> None let subst_univs_context_with_def def usubst (ctx, cst) = - (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst) + (Univ.LSet.diff ctx def, Universes.subst_univs_constraints usubst cst) let normalize_variables uctx = let normalized_variables, undef, def, subst = diff --git a/engine/universes.ml b/engine/universes.ml index 30490ec56..eaddf98a8 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -181,6 +181,30 @@ let enforce_eq_instances_univs strict x y c = (fun x y -> Constraints.add (Universe.make x, d, Universe.make y)) ax ay c +let enforce_univ_constraint (u,d,v) = + match d with + | Eq -> enforce_eq u v + | Le -> enforce_leq u v + | Lt -> enforce_leq (super u) v + +let subst_univs_level fn l = + try Some (fn l) + with Not_found -> None + +let subst_univs_constraint fn (u,d,v as c) cstrs = + let u' = subst_univs_level fn u in + let v' = subst_univs_level fn v in + match u', v' with + | None, None -> Constraint.add c cstrs + | Some u, None -> enforce_univ_constraint (u,d,Universe.make v) cstrs + | None, Some v -> enforce_univ_constraint (Universe.make u,d,v) cstrs + | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs + +let subst_univs_constraints subst csts = + Constraint.fold + (fun c cstrs -> subst_univs_constraint subst c cstrs) + csts Constraint.empty + let subst_univs_universe_constraint fn (u,d,v) = let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in if Universe.equal u' v' then None @@ -519,13 +543,60 @@ let choose_canonical ctx flexible algs s = let canon = LSet.choose algs in canon, (global, rigid, LSet.remove canon flexible) +let level_subst_of f = + fun l -> + try let u = f l in + match Universe.level u with + | None -> l + | Some l -> l + with Not_found -> l + +let subst_univs_fn_constr f c = + let changed = ref false in + let fu = Univ.subst_univs_universe f in + let fi = Univ.Instance.subst_fn (level_subst_of f) in + let rec aux t = + match kind t with + | Sort (Sorts.Type u) -> + let u' = fu u in + if u' == u then t else + (changed := true; mkSort (Sorts.sort_of_univ u')) + | Const (c, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; mkConstU (c, u')) + | Ind (i, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; mkIndU (i, u')) + | Construct (c, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; mkConstructU (c, u')) + | _ -> map aux t + in + let c' = aux c in + if !changed then c' else c + +let subst_univs_constr subst c = + if Univ.is_empty_subst subst then c + else + let f = Univ.make_subst subst in + subst_univs_fn_constr f c + +let subst_univs_constr = + if Flags.profile then + let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in + CProfile.profile2 subst_univs_constr_key subst_univs_constr + else subst_univs_constr + let subst_univs_fn_puniverses lsubst (c, u as cu) = let u' = Instance.subst_fn lsubst u in if u' == u then cu else (c, u') let nf_evars_and_universes_opt_subst f subst = let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in - let lsubst = Univ.level_subst_of subst in + let lsubst = level_subst_of subst in let rec aux c = match kind c with | Evar (evk, args) -> @@ -605,7 +676,7 @@ let normalize_opt_subst ctx = in !ectx type universe_opt_subst = Universe.t option universe_map - + let make_opt_subst s = fun x -> (match Univ.LMap.find x s with @@ -614,8 +685,7 @@ let make_opt_subst s = let subst_opt_univs_constr s = let f = make_opt_subst s in - Vars.subst_univs_fn_constr f - + subst_univs_fn_constr f let normalize_univ_variables ctx = let ctx = normalize_opt_subst ctx in diff --git a/engine/universes.mli b/engine/universes.mli index 1a98d969b..130dcf8bb 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -154,6 +154,11 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t -> module UF : Unionfind.PartitionSig with type elt = Level.t +val level_subst_of : universe_subst_fn -> universe_level_subst_fn +val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t + +val subst_univs_constr : universe_subst -> constr -> constr + type universe_opt_subst = Universe.t option universe_map val make_opt_subst : universe_opt_subst -> universe_subst_fn diff --git a/ide/config_lexer.mli b/ide/config_lexer.mli new file mode 100644 index 000000000..0c0c5d1e7 --- /dev/null +++ b/ide/config_lexer.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val print_file : string -> string list Util.String.Map.t -> unit +val load_file : string -> string list Util.String.Map.t diff --git a/ide/coq_commands.mli b/ide/coq_commands.mli new file mode 100644 index 000000000..53026be38 --- /dev/null +++ b/ide/coq_commands.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val tactics : string list list +val commands : string list list +val state_preserving : string list diff --git a/ide/coq_lex.mli b/ide/coq_lex.mli new file mode 100644 index 000000000..417e0a76f --- /dev/null +++ b/ide/coq_lex.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val delimit_sentences : (int -> GText.tag -> unit) -> string -> unit + +exception Unterminated diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 8d99cc3e6..6e330c62b 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -55,6 +55,8 @@ let os_specific_init () = () (** Win32 *) +IFDEF WIN32 THEN + (* On win32, we add the directory of coqide to the PATH at launch-time (this used to be done in a .bat script). *) @@ -86,7 +88,6 @@ let reroute_stdout_stderr () = (* We also provide specific kill and interrupt functions. *) -IFDEF WIN32 THEN external win32_kill : int -> unit = "win32_kill" external win32_interrupt : int -> unit = "win32_interrupt" let () = diff --git a/ide/coqide_main.mli b/ide/coqide_main.mli new file mode 100644 index 000000000..e1555ba2e --- /dev/null +++ b/ide/coqide_main.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This empty file avoids a race condition that occurs when compiling a .ml file + that does not have a corresponding .mli file *) diff --git a/ide/coqide_ui.mli b/ide/coqide_ui.mli new file mode 100644 index 000000000..9f6fa5635 --- /dev/null +++ b/ide/coqide_ui.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val init : unit -> unit +val ui_m : GAction.ui_manager diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index f0575e325..7c0a7495a 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -7,11 +7,7 @@ (************************************************************************) let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0) -let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0) let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0) -let bn = Glib.Utf8.to_unichar "\n" ~pos:(ref 0) -let space = Glib.Utf8.to_unichar " " ~pos:(ref 0) -let tab = Glib.Utf8.to_unichar "\t" ~pos:(ref 0) (* TODO: avoid num and prime at the head of a word *) @@ -30,17 +26,6 @@ let ends_word (it:GText.iter) = not (is_word_char c) ) - -let inside_word (it:GText.iter) = - let c = it#char in - not (starts_word it) && - not (ends_word it) && - is_word_char c - - -let is_on_word_limit (it:GText.iter) = inside_word it || ends_word it - - let find_word_start (it:GText.iter) = let rec step_to_start it = Minilib.log "Find word start"; @@ -72,100 +57,6 @@ let get_word_around (it:GText.iter) = let stop = find_word_end it in start,stop - -let rec complete_backward w (it:GText.iter) = - Minilib.log "Complete backward..."; - match it#backward_search w with - | None -> (Minilib.log "backward_search failed";None) - | Some (start,stop) -> - Minilib.log ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset)); - if starts_word start then - let ne = find_word_end stop in - if ne#compare stop = 0 - then complete_backward w start - else Some (start,stop,ne) - else complete_backward w start - - -let rec complete_forward w (it:GText.iter) = - Minilib.log "Complete forward..."; - match it#forward_search w with - | None -> None - | Some (start,stop) -> - if starts_word start then - let ne = find_word_end stop in - if ne#compare stop = 0 then - complete_forward w stop - else Some (stop,stop,ne) - else complete_forward w stop - - -let find_comment_end (start:GText.iter) = - let rec find_nested_comment (search_start:GText.iter) (search_end:GText.iter) (comment_end:GText.iter) = - match (search_start#forward_search ~limit:search_end "(*"),(comment_end#forward_search "*)") with - | None,_ -> comment_end - | Some _, None -> raise Not_found - | Some (_,next_search_start),Some (next_search_end,next_comment_end) -> - find_nested_comment next_search_start next_search_end next_comment_end - in - match start#forward_search "*)" with - | None -> raise Not_found - | Some (search_end,comment_end) -> find_nested_comment start search_end comment_end - - -let rec find_string_end (start:GText.iter) = - let dblquote = int_of_char '"' in - let rec escaped_dblquote c = - (c#char = dblquote) && not (escaped_dblquote c#backward_char) - in - match start#forward_search "\"" with - | None -> raise Not_found - | Some (stop,next_start) -> - if escaped_dblquote stop#backward_char - then find_string_end next_start - else next_start - - -let rec find_next_sentence (from:GText.iter) = - match (from#forward_search ".") with - | None -> raise Not_found - | Some (non_vernac_search_end,next_sentence) -> - match from#forward_search ~limit:non_vernac_search_end "(*",from#forward_search ~limit:non_vernac_search_end "\"" with - | None,None -> - if Glib.Unichar.isspace next_sentence#char || next_sentence#compare next_sentence#forward_char == 0 - then next_sentence else find_next_sentence next_sentence - | None,Some (_,string_search_start) -> find_next_sentence (find_string_end string_search_start) - | Some (_,comment_search_start),None -> find_next_sentence (find_comment_end comment_search_start) - | Some (_,comment_search_start),Some (_,string_search_start) -> - find_next_sentence ( - if comment_search_start#compare string_search_start < 0 - then find_comment_end comment_search_start - else find_string_end string_search_start) - - -let find_nearest_forward (cursor:GText.iter) targets = - let fold_targets acc target = - match cursor#forward_search target,acc with - | Some (t_start,_),Some nearest when (t_start#compare nearest < 0) -> Some t_start - | Some (t_start,_),None -> Some t_start - | _ -> acc - in - match List.fold_left fold_targets None targets with - | None -> raise Not_found - | Some nearest -> nearest - - -let find_nearest_backward (cursor:GText.iter) targets = - let fold_targets acc target = - match cursor#backward_search target,acc with - | Some (t_start,_),Some nearest when (t_start#compare nearest > 0) -> Some t_start - | Some (t_start,_),None -> Some t_start - | _ -> acc - in - match List.fold_left fold_targets None targets with - | None -> raise Not_found - | Some nearest -> nearest - (** On double-click on a view, select the whole word. This is a workaround for a deficient word handling in TextView. *) let fix_double_click self = diff --git a/ide/gtk_parsing.mli b/ide/gtk_parsing.mli new file mode 100644 index 000000000..b54f731b3 --- /dev/null +++ b/ide/gtk_parsing.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val fix_double_click : + < buffer : < get_iter : [> `INSERT ] -> GText.iter; + move_mark : [> `INSERT | `SEL_BOUND ] -> + where:GText.iter -> unit; + .. >; + event : < connect : + < button_press : + callback:([> `TWO_BUTTON_PRESS ] Gdk.event -> + bool) -> + 'a; + .. >; + .. >; + .. > -> + unit +val starts_word : GText.iter -> bool +val ends_word : GText.iter -> bool +val find_word_start : GText.iter -> GText.iter +val find_word_end : GText.iter -> GText.iter diff --git a/ide/ide_slave.mli b/ide/ide_slave.mli new file mode 100644 index 000000000..e1555ba2e --- /dev/null +++ b/ide/ide_slave.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This empty file avoids a race condition that occurs when compiling a .ml file + that does not have a corresponding .mli file *) diff --git a/ide/macos_prehook.mli b/ide/macos_prehook.mli new file mode 100644 index 000000000..e1555ba2e --- /dev/null +++ b/ide/macos_prehook.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This empty file avoids a race condition that occurs when compiling a .ml file + that does not have a corresponding .mli file *) diff --git a/ide/nanoPG.mli b/ide/nanoPG.mli new file mode 100644 index 000000000..3ad8435b5 --- /dev/null +++ b/ide/nanoPG.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val get_documentation : unit -> string +val init : GWindow.window -> Session.session Wg_Notebook.typed_notebook -> + GAction.action_group list -> unit diff --git a/ide/utf8_convert.mli b/ide/utf8_convert.mli new file mode 100644 index 000000000..06a131a68 --- /dev/null +++ b/ide/utf8_convert.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val f : string -> string diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 3ecb3d321..6e5c0f851 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -84,7 +84,7 @@ val names_of_local_assums : local_binder_expr list -> Name.t located list (** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into account. *) -(** { 6 Folds and maps } *) +(** {6 Folds and maps} *) (** Used in typeclasses *) val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) -> diff --git a/interp/declare.ml b/interp/declare.ml index d1b79ffcd..55f825c25 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -104,7 +104,7 @@ let discharge_constant ((sp, kn), obj) = let con = Constant.make1 kn in let from = Global.lookup_constant con in let modlist = replacement_context () in - let hyps,subst,uctx = section_segment_of_constant con in + let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in let abstract = (named_of_variable_context hyps, subst, uctx) in let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in @@ -333,7 +333,8 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in - let sechyps, _, _ as info = section_segment_of_mutual_inductive mind in + let info = section_segment_of_mutual_inductive mind in + let sechyps = info.Lib.abstr_ctx in Some (discharged_hyps kn sechyps, Discharge.process_inductive info repl mie) diff --git a/interp/discharge.ml b/interp/discharge.ml index 5b4b5f67b..75bfca307 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -78,8 +78,8 @@ let refresh_polymorphic_type_of_inductive (_,mip) = let ctx = List.rev mip.mind_arity_ctxt in mkArity (List.rev ctx, Type ar.template_level), true -let process_inductive (section_decls,_,_ as info) modlist mib = - let section_decls = Lib.named_of_variable_context section_decls in +let process_inductive info modlist mib = + let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in let nparamdecls = Context.Rel.length mib.mind_params_ctxt in let subst, ind_univs = match mib.mind_universes with diff --git a/interp/impargs.ml b/interp/impargs.ml index 3105214d5..ed1cd5276 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -548,7 +548,7 @@ let discharge_implicits (_,(req,l)) = | ImplConstant (con,flags) -> (try let con' = pop_con con in - let vars,_,_ = section_segment_of_constant con in + let vars = variable_section_segment_of_reference (ConstRef con) in let extra_impls = impls_of_context vars in let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in let l' = [ConstRef con',newimpls] in diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 7b921d35b..23a578d99 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -168,38 +168,47 @@ let on_body ml hy f = function { Opaqueproof.modlist = ml; abstract = hy } o) let expmod_constr_subst cache modlist subst c = + let subst = Univ.make_instance_subst subst in let c = expmod_constr cache modlist c in Vars.subst_univs_level_constr subst c -let cook_constr { Opaqueproof.modlist ; abstract } c = +let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c = let cache = RefTable.create 13 in - let expmod = expmod_constr_subst cache modlist (pi2 abstract) in - let hyps = Context.Named.map expmod (pi1 abstract) in + let expmod = expmod_constr_subst cache modlist subst in + let hyps = Context.Named.map expmod vars in abstract_constant_body (expmod c) hyps -let lift_univs cb subst = +let lift_univs cb subst auctx0 = match cb.const_universes with - | Monomorphic_const ctx -> subst, (Monomorphic_const ctx) - | Polymorphic_const auctx -> - if (Univ.LMap.is_empty subst) then - subst, (Polymorphic_const auctx) + | Monomorphic_const ctx -> + assert (AUContext.is_empty auctx0); + subst, (Monomorphic_const ctx) + | Polymorphic_const auctx -> + (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract + context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length, + and another abstract context relative to the former context + [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}], + construct the lifted abstract universe context + [0 ... n - 1 n ... n + m - 1 |= + C{0, ... n - 1} ∪ + C'{0, ..., n - 1, n, ..., n + m - 1} ] + together with the instance + [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)]. + *) + if (Univ.Instance.is_empty subst) then + (** Still need to take the union for the constraints between globals *) + subst, (Polymorphic_const (AUContext.union auctx0 auctx)) else - let len = Univ.LMap.cardinal subst in - let rec gen_subst i acc = - if i < 0 then acc - else - let acc = Univ.LMap.add (Level.var i) (Level.var (i + len)) acc in - gen_subst (pred i) acc - in - let subst = gen_subst (Univ.AUContext.size auctx - 1) subst in - let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in - subst, (Polymorphic_const auctx') + let ainst = Univ.make_abstract_instance auctx in + let subst = Instance.append subst ainst in + let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in + subst, (Polymorphic_const (AUContext.union auctx0 auctx')) let cook_constant ~hcons env { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in - let usubst, univs = lift_univs cb usubst in + let usubst, univs = lift_univs cb usubst abs_ctx in let expmod = expmod_constr_subst cache modlist usubst in let hyps = Context.Named.map expmod abstract in let map c = @@ -234,13 +243,6 @@ let cook_constant ~hcons env { from = cb; info } = proj_eta = etab, etat; proj_type = ty'; proj_body = c' } in - let univs = - match univs with - | Monomorphic_const ctx -> - assert (AUContext.is_empty abs_ctx); univs - | Polymorphic_const auctx -> - Polymorphic_const (AUContext.union abs_ctx auctx) - in { cook_body = body; cook_type = typ; diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 1f2ae0b6c..b117f8714 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -879,9 +879,13 @@ let abstract_inductive_universes iu = match iu with | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) | Polymorphic_ind_entry ctx -> - let (inst, auctx) = Univ.abstract_universes ctx in (inst, Polymorphic_ind auctx) + let (inst, auctx) = Univ.abstract_universes ctx in + let inst = Univ.make_instance_subst inst in + (inst, Polymorphic_ind auctx) | Cumulative_ind_entry cumi -> - let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi) + let (inst, acumi) = Univ.abstract_cumulativity_info cumi in + let inst = Univ.make_instance_subst inst in + (inst, Cumulative_ind acumi) let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index f7e755f00..b7eb481ee 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -94,8 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let ctx = Univ.ContextSet.of_context ctx in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx | Polymorphic_const uctx -> - let subst, ctx = Univ.abstract_universes ctx in - let c = Vars.subst_univs_level_constr subst c in + let inst, ctx = Univ.abstract_universes ctx in + let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in let () = if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then error_incorrect_with_constraint lab diff --git a/kernel/names.mli b/kernel/names.mli index 709ebeb7f..b1e8efd8d 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -40,19 +40,16 @@ sig (** Hash over identifiers. *) val is_valid : string -> bool - (** Check that a string may be converted to an identifier. - @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) + (** Check that a string may be converted to an identifier. *) val of_bytes : bytes -> t val of_string : string -> t (** Converts a string into an identifier. - @raise UserError if the string is invalid as an identifier. - @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) + @raise UserError if the string is invalid as an identifier. *) val of_string_soft : string -> t (** Same as {!of_string} except that any string made of supported UTF-8 characters is accepted. - @raise UserError if the string is invalid as an UTF-8 string. - @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) + @raise UserError if the string is invalid as an UTF-8 string. *) val to_string : t -> string (** Converts a identifier into an string. *) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 45a62d55a..c2fcfbfd6 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } + abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t } type proofterm = (constr * Univ.ContextSet.t) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 20d76ce23..c8339e6eb 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -49,7 +49,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } + abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t } (* The type has two caveats: 1) cook_constr is defined after diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 2e4426d62..5f501bff1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -232,6 +232,7 @@ let abstract_constant_universes = function Univ.empty_level_subst, Monomorphic_const uctx | Polymorphic_const_entry uctx -> let sbst, auctx = Univ.abstract_universes uctx in + let sbst = Univ.make_instance_subst sbst in sbst, Polymorphic_const auctx let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = @@ -300,21 +301,29 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - let poly, univsctx = match c.const_entry_universes with - | Monomorphic_const_entry univs -> false, univs - | Polymorphic_const_entry univs -> true, Univ.ContextSet.of_context univs - in - let ctx = Univ.ContextSet.union univsctx ctx in let body, ctx, _ = match trust with | Pure -> body, ctx, [] | SideEffects _ -> inline_side_effects env body ctx side_eff in - let env = push_context_set ~strict:(not poly) ctx env in - let ctx = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context ctx) - else Monomorphic_const_entry ctx + let env, usubst, univs = match c.const_entry_universes with + | Monomorphic_const_entry univs -> + let ctx = Univ.ContextSet.union univs ctx in + let env = push_context_set ~strict:true ctx env in + env, Univ.empty_level_subst, Monomorphic_const ctx + | Polymorphic_const_entry uctx -> + (** Ensure not to generate internal constraints in polymorphic mode. + The only way for this to happen would be that either the body + contained deferred universes, or that it contains monomorphic + side-effects. The first property is ruled out by upper layers, + and the second one is ensured by the fact we currently + unconditionally export side-effects from polymorphic definitions, + i.e. [trust] is always [Pure]. *) + let () = assert (Univ.ContextSet.is_empty ctx) in + let env = push_context ~strict:false uctx env in + let sbst, auctx = Univ.abstract_universes uctx in + let sbst = Univ.make_instance_subst sbst in + env, sbst, Polymorphic_const auctx in - let usubst, univs = abstract_constant_universes ctx in let j = infer env body in let typ = match typ with | None -> diff --git a/kernel/univ.ml b/kernel/univ.ml index 8cf9028fb..f72f6f26a 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -686,12 +686,6 @@ let enforce_leq u v c = let enforce_leq_level u v c = if Level.equal u v then c else Constraint.add (u,Le,v) c -let enforce_univ_constraint (u,d,v) = - match d with - | Eq -> enforce_eq u v - | Le -> enforce_leq u v - | Lt -> enforce_leq (super u) v - (* Miscellaneous functions to remove or test local univ assumed to occur in a universe *) @@ -718,14 +712,6 @@ type universe_level_subst = universe_level universe_map (** A full substitution might involve algebraic universes *) type universe_subst = universe universe_map -let level_subst_of f = - fun l -> - try let u = f l in - match Universe.level u with - | None -> l - | Some l -> l - with Not_found -> l - module Instance : sig type t = Level.t array @@ -1128,24 +1114,6 @@ let subst_univs_universe fn ul = List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u)) substs nosubst -let subst_univs_level fn l = - try Some (fn l) - with Not_found -> None - -let subst_univs_constraint fn (u,d,v as c) cstrs = - let u' = subst_univs_level fn u in - let v' = subst_univs_level fn v in - match u', v' with - | None, None -> Constraint.add c cstrs - | Some u, None -> enforce_univ_constraint (u,d,make v) cstrs - | None, Some v -> enforce_univ_constraint (make u,d,v) cstrs - | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs - -let subst_univs_constraints subst csts = - Constraint.fold - (fun c cstrs -> subst_univs_constraint subst c cstrs) - csts Constraint.empty - let make_instance_subst i = let arr = Instance.to_array i in Array.fold_left_i (fun i acc l -> @@ -1168,7 +1136,7 @@ let abstract_universes ctx = (UContext.constraints ctx) in let ctx = UContext.make (instance, cstrs) in - subst, ctx + instance, ctx let abstract_cumulativity_info (univcst, substcst) = let instance, univcst = abstract_universes univcst in diff --git a/kernel/univ.mli b/kernel/univ.mli index 459394439..63bef1b81 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -238,8 +238,6 @@ type universe_level_subst_fn = Level.t -> Level.t type universe_subst = Universe.t universe_map type universe_level_subst = Level.t universe_map -val level_subst_of : universe_subst_fn -> universe_level_subst_fn - (** {6 Universe instances} *) module Instance : @@ -461,18 +459,21 @@ val is_empty_subst : universe_subst -> bool val make_subst : universe_subst -> universe_subst_fn val subst_univs_universe : universe_subst_fn -> Universe.t -> Universe.t -val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t +(** Only user in the kernel is template polymorphism. Ideally we get rid of + this code if it goes away. *) (** Substitution of instances *) val subst_instance_instance : Instance.t -> Instance.t -> Instance.t val subst_instance_universe : Instance.t -> Universe.t -> Universe.t val make_instance_subst : Instance.t -> universe_level_subst -val make_inverse_instance_subst : Instance.t -> universe_level_subst +(** Creates [u(0) ↦ 0; ...; u(n-1) ↦ n - 1] out of [u(0); ...; u(n - 1)] *) -val abstract_universes : UContext.t -> universe_level_subst * AUContext.t +val make_inverse_instance_subst : Instance.t -> universe_level_subst -val abstract_cumulativity_info : CumulativityInfo.t -> universe_level_subst * ACumulativityInfo.t +val abstract_universes : UContext.t -> Instance.t * AUContext.t +val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t +(** TODO: move universe abstraction out of the kernel *) val make_abstract_instance : AUContext.t -> Instance.t diff --git a/kernel/vars.ml b/kernel/vars.ml index eae917b5a..b3b3eff62 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -235,49 +235,6 @@ let subst_vars subst c = substn_vars 1 subst c (** Universe substitutions *) open Constr -let subst_univs_fn_puniverses fn = - let f = Univ.Instance.subst_fn fn in - fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') - -let subst_univs_fn_constr f c = - let changed = ref false in - let fu = Univ.subst_univs_universe f in - let fi = Univ.Instance.subst_fn (Univ.level_subst_of f) in - let rec aux t = - match kind t with - | Sort (Sorts.Type u) -> - let u' = fu u in - if u' == u then t else - (changed := true; mkSort (Sorts.sort_of_univ u')) - | Const (c, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; mkConstU (c, u')) - | Ind (i, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; mkIndU (i, u')) - | Construct (c, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; mkConstructU (c, u')) - | _ -> map aux t - in - let c' = aux c in - if !changed then c' else c - -let subst_univs_constr subst c = - if Univ.is_empty_subst subst then c - else - let f = Univ.make_subst subst in - subst_univs_fn_constr f c - -let subst_univs_constr = - if Flags.profile then - let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in - CProfile.profile2 subst_univs_constr_key subst_univs_constr - else subst_univs_constr - let subst_univs_level_constr subst c = if Univ.is_empty_level_subst subst then c else diff --git a/kernel/vars.mli b/kernel/vars.mli index 964de4e95..b74d25260 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -129,12 +129,6 @@ val subst_var : Id.t -> constr -> constr open Univ -val subst_univs_fn_constr : universe_subst_fn -> constr -> constr -val subst_univs_fn_puniverses : universe_level_subst_fn -> - 'a puniverses -> 'a puniverses - -val subst_univs_constr : universe_subst -> constr -> constr - (** Level substitutions for polymorphism. *) val subst_univs_level_constr : universe_level_subst -> constr -> constr diff --git a/library/lib.ml b/library/lib.ml index 499e2ae21..971089c17 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -417,8 +417,11 @@ let find_opening_node id = type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list -type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t - +type abstr_info = { + abstr_ctx : variable_context; + abstr_subst : Univ.Instance.t; + abstr_uctx : Univ.AUContext.t; +} type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t type secentry = @@ -483,8 +486,12 @@ let add_section_replacement f g poly hyps = let inst = Univ.UContext.instance ctx in let subst, ctx = Univ.abstract_universes ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (inst,args) exps, - g (sechyps,subst,ctx) abs)::sl + let info = { + abstr_ctx = sechyps; + abstr_subst = subst; + abstr_uctx = ctx; + } in + sectab := (vars,f (inst,args) exps, g info abs) :: sl let add_section_kn poly kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in @@ -502,12 +509,21 @@ let section_segment_of_constant con = let section_segment_of_mutual_inductive kn = Names.Mindmap.find kn (snd (pi3 (List.hd !sectab))) -let variable_section_segment_of_reference = function - | ConstRef con -> pi1 (section_segment_of_constant con) - | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - pi1 (section_segment_of_mutual_inductive kn) - | _ -> [] - +let empty_segment = { + abstr_ctx = []; + abstr_subst = Univ.Instance.empty; + abstr_uctx = Univ.AUContext.empty; +} + +let section_segment_of_reference = function +| ConstRef c -> section_segment_of_constant c +| IndRef (kn,_) | ConstructRef ((kn,_),_) -> + section_segment_of_mutual_inductive kn +| VarRef _ -> empty_segment + +let variable_section_segment_of_reference gr = + (section_segment_of_reference gr).abstr_ctx + let section_instance = function | VarRef id -> let eq = function @@ -654,15 +670,10 @@ let discharge_con cst = let discharge_inductive (kn,i) = (discharge_kn kn,i) -let discharge_abstract_universe_context (_, subst, abs_ctx) auctx = +let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx = let open Univ in - let len = LMap.cardinal subst in - let rec gen_subst i acc = - if i < 0 then acc - else - let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in - gen_subst (pred i) acc - in - let subst = gen_subst (AUContext.size auctx - 1) subst in + let ainst = make_abstract_instance auctx in + let subst = Instance.append subst ainst in + let subst = make_instance_subst subst in let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in subst, AUContext.union abs_ctx auctx diff --git a/library/lib.mli b/library/lib.mli index 721e2896f..cf75d5f8c 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -153,13 +153,22 @@ val init : unit -> unit (** {6 Section management for discharge } *) type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list -type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t +type abstr_info = private { + abstr_ctx : variable_context; + (** Section variables of this prefix *) + abstr_subst : Univ.Instance.t; + (** Actual names of the abstracted variables *) + abstr_uctx : Univ.AUContext.t; + (** Universe quantification, same length as the substitution *) +} val instance_from_variable_context : variable_context -> Names.Id.t array val named_of_variable_context : variable_context -> Context.Named.t val section_segment_of_constant : Names.Constant.t -> abstr_info val section_segment_of_mutual_inductive: Names.MutInd.t -> abstr_info +val section_segment_of_reference : Globnames.global_reference -> abstr_info + val variable_section_segment_of_reference : Globnames.global_reference -> variable_context val section_instance : Globnames.global_reference -> Univ.Instance.t * Names.Id.t array diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index cf5125757..3e3965b94 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -1125,3 +1125,12 @@ VERNAC COMMAND EXTEND OptimizeProof | [ "Optimize" "Heap" ] => [ Vernac_classifier.classify_as_proofstep ] -> [ Gc.compact () ] END + +(** tactic analogous to "OPTIMIZE HEAP" *) + +let tclOPTIMIZE_HEAP = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ())) + +TACTIC EXTEND optimize_heap +| [ "optimize_heap" ] -> [ tclOPTIMIZE_HEAP ] +END diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index d59102b6c..8ac471404 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -40,16 +40,10 @@ let subst_rename_args (subst, (_, (r, names as orig))) = let r' = fst (subst_global subst r) in if r==r' then orig else (r', names) -let section_segment_of_reference = function - | ConstRef con -> Lib.section_segment_of_constant con - | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - Lib.section_segment_of_mutual_inductive kn - | _ -> [], Univ.LMap.empty, Univ.AUContext.empty - let discharge_rename_args = function | _, (ReqGlobal (c, names), _ as req) -> (try - let vars,_,_ = section_segment_of_reference c in + let vars = Lib.variable_section_segment_of_reference c in let c' = pop_global_reference c in let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in let names' = var_names @ names in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index ac8846854..78de0437d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -121,10 +121,10 @@ module ReductionBehaviour = struct let r' = fst (subst_global subst r) in if r==r' then orig else (r',o) let discharge = function - | _,(ReqGlobal (ConstRef c, req), (_, b)) -> + | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) -> let b = - if Lib.is_in_section (ConstRef c) then - let vars, _, _ = Lib.section_segment_of_constant c in + if Lib.is_in_section gr then + let vars = Lib.variable_section_segment_of_reference gr in let extra = List.length vars in let nargs' = if b.b_nargs = max_int then max_int diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index f153b6341..3f947fd23 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -219,7 +219,8 @@ let discharge_class (_,cl) = in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in if cl_impl' == cl.cl_impl then cl else - let ctx, _, _ as info = abs_context cl in + let info = abs_context cl in + let ctx = info.Lib.abstr_ctx in let ctx, subst = rel_of_variable_context ctx in let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in let context = discharge_context ctx (subst, usubst) cl.cl_context in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b41fb4e4d..8df8f8474 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -module CVars = Vars - open CErrors open Pp open Util @@ -1527,7 +1525,7 @@ let indirectly_dependent sigma c d decls = let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in let sigma, subst = nf_univ_variables sigma in - (sigma, EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c)))) + (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c)))) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1617,7 +1615,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = | Some (sigma,_,l) -> let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in let univs, subst = nf_univ_variables sigma in - Some (sigma,EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) + Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) let make_eq_test env evd c = let out cstr = diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 167d6bda0..d04bdb652 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -343,16 +343,15 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now if poly || now then let make_body t (c, eff) = let body = c in - let typ = - if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then - nf t - else t + let allow_deferred = + not poly && (keep_body_ucst_separate || + not (Safe_typing.empty_private_constants = eff)) in + let typ = if allow_deferred then t else nf t in let env = Global.env () in let used_univs_body = Univops.universes_of_constr env body in let used_univs_typ = Univops.universes_of_constr env typ in - if keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff) then + if allow_deferred then let initunivs = UState.const_univ_entry ~poly initial_euctx in let ctx = constrain_variables universes in (* For vi2vo compilation proofs are computed now but we need to diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index 07689389f..706d36e1d 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -71,7 +71,7 @@ module type Task = sig (** Extra arguments of the task kind, for -toploop *) val extra_env : unit -> string array - (** {5} Master API, it is run by the master, on a thread *) + (** {5 Master API, it is run by the master, on a thread} *) (** [request_of_task status t] takes the [status] of the worker and a task [t] and creates the corresponding [Some request] to be @@ -116,8 +116,8 @@ module type Task = sig (** [forward_feedback fb] sends fb to all the workers. *) val forward_feedback : Feedback.feedback -> unit - (** {5} Worker API, it is run by worker, on a different fresh - process *) + (** {5 Worker API, it is run by worker, on a different fresh + process} *) (** [perform in] synchronously processes a request [in] *) val perform : request -> response diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e1bf32f3c..bc2fea2bd 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -121,8 +121,7 @@ let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in let ctx = Evd.normalize_evar_universe_context univs in - let c = Vars.subst_univs_fn_constr - (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in + let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) else Monomorphic_const_entry (UState.context_set ctx) diff --git a/test-suite/Makefile b/test-suite/Makefile index de669218c..16a56f440 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -40,6 +40,7 @@ coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source coqtopcompile := $(coqtop) -compile coqdep := $(BIN)coqdep -coqlib $(LIB) +VERBOSE?= SHOW := $(if $(VERBOSE),@true,@echo) HIDE := $(if $(VERBOSE),,@) REDIR := $(if $(VERBOSE),,> /dev/null 2>&1) @@ -174,10 +175,20 @@ summary.log: # if not on travis we can get the log files (they're just there for a # local build, and downloadable on GitLab) +PRINT_LOGS?= +TRAVIS?= # special because we want to print travis_fold directives +ifdef APPVEYOR +PRINT_LOGS:=APPVEYOR +else +ifdef CIRCLECI +PRINT_LOGS:=CIRCLECI +endif #CIRCLECI +endif #APPVEYOR + report: summary.log $(HIDE)bash save-logs.sh $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi - $(HIDE)if [ "(" -n "${APPVEYOR}" ")" -o "(" -n "${CIRCLECI}" ")" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi + $(HIDE)if [ -n "${PRINT_LOGS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### diff --git a/test-suite/README.md b/test-suite/README.md new file mode 100644 index 000000000..1d1195646 --- /dev/null +++ b/test-suite/README.md @@ -0,0 +1,75 @@ +# Coq Test Suite + +The test suite can be run from the Coq root directory by `make test-suite`. +This does a clean step first, so if you've already run it, then change something, +you'll have to do a lot of work again. + +If you run `make` from the `test-suite` directory, there is no clean step. +You can also run `make aaa/bbb/ccc.v.log` to build the log for one test, +or `make ddd` where `ddd` is on of the sub-directories of `test-suite` +to just build the logs for that directory. +In these cases, a summary is not printed, but can be generated by `make summary`. + +`make -B` can be used to rerun tests ( -B meaning always remake). + +From the `test-suite` directory, `make report` (included in `make +all`) prints a summary of which tests failed using the produced log +files (this still works when only some tests are built as described +above). Setting the `PRINT_LOGS` variable will make it print the logs +of the failing tests. + +For instance, running the following in the `test-suite` directory: + +```bash +$ echo Fail. > success/fail.v # make some failing test + +$ make +TEST prerequisite/make_local.v +... +TEST success/fail.v +... +BUILDING SUMMARY FILE +FAILURES + success/fail.v...Error! (should be accepted) +Makefile:189: recipe for target 'all failed +make: *** [report] Error 1 + +$ make report PRINT_LOGS=1 +BUILDING SUMMARY FILE +logs/success/fail.v.log +==========> TESTING success/fail.v <========== +Welcome to Coq (version information) +Skipping rcfile loading. +File "/path/to/success/fail.v", line 1, characters 4-5: +Error: +Syntax error: [vernac:Vernac.vernac_control] expected after 'Fail' (in [vernac:Vernac.vernac_control]). + +0m0.000000s 0m0.000000s +0m0.040000s 0m0.000000s +==========> FAILURE <========== + success/fail.v...Error! (should be accepted) + +FAILURES + success/fail.v...Error! (should be accepted) +Makefile:189: recipe for target 'report' failed +make: *** [report] Error 1 + +$ echo 'Comments "foo".' > success/fail.v + +$ make +TEST success/fail.v +BUILDING SUMMARY FILE +NO FAILURES +``` + +See [`test-suite/Makefile`](/test-suite/Makefile) for more information. + +## Adding a test + +Regression tests for closed bugs should be added to `test-suite/bugs/closed`, as `1234.v` where `1234` is the bug number. +Files in this directory are tested for successful compilation. +When you fix a bug, you should usually add a regression test here as well. + +The error "(bug seems to be opened, please check)" when running `make test-suite` means that a test in `bugs/closed` failed to compile. + +There are also output tests in `test-suite/output` which consist of a `.v` file and a `.out` file with the expected output. diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 898af5590..2439d3f37 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -31,16 +31,16 @@ coq_makefile -f _CoqProject -o Makefile make cleanall make make-pretty-timed-after TGTS="all" -j1 || exit $? rm -f time-of-build-before.log -make print-pretty-timed-diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log +make print-pretty-timed-diff TIMING_SORT_BY=diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log cp ../before/time-of-build-before.log ./ -make print-pretty-timed-diff || exit $? +make print-pretty-timed-diff TIMING_SORT_BY=diff || exit $? INFINITY="∞" INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase for ext in "" .desired; do for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do - cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed + cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed done done for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do @@ -74,7 +74,7 @@ echo for ext in "" .desired; do for file in A.v.timing.diff; do - cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/+/-/g' | sort > ${file}${ext}.processed + cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/ *$//g' | sed s'/+/-/g' | sort > ${file}${ext}.processed done done for file in A.v.timing.diff; do diff --git a/test-suite/output/optimize_heap.out b/test-suite/output/optimize_heap.out new file mode 100644 index 000000000..94a0b1911 --- /dev/null +++ b/test-suite/output/optimize_heap.out @@ -0,0 +1,8 @@ +1 subgoal + + ============================ + True +1 subgoal + + ============================ + True diff --git a/test-suite/output/optimize_heap.v b/test-suite/output/optimize_heap.v new file mode 100644 index 000000000..e566bd7ba --- /dev/null +++ b/test-suite/output/optimize_heap.v @@ -0,0 +1,7 @@ +(* optimize_heap should not affect the proof state *) + +Goal True. + idtac. + Show. + optimize_heap. + Show. diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v index b736b734f..aa8da5336 100644 --- a/test-suite/success/abstract_poly.v +++ b/test-suite/success/abstract_poly.v @@ -17,4 +17,4 @@ intros m n P e p. abstract (rewrite e in p; exact p). Defined. -Check bar_subproof@{Set Set Set}. +Check bar_subproof@{Set Set}. diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 9b4071085..ead08b3eb 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -16,6 +16,8 @@ Implicit Types k l p q r : nat. Section Between. Variables P Q : nat -> Prop. + (** The [between] type expresses the concept + [forall i: nat, k <= i < l -> P i.]. *) Inductive between k : nat -> Prop := | bet_emp : between k k | bet_S : forall l, between k l -> P l -> between k (S l). @@ -47,6 +49,8 @@ Section Between. induction 1; auto with arith. Qed. + (** The [exists_between] type expresses the concept + [exists i: nat, k <= i < l /\ Q i]. *) Inductive exists_between k : nat -> Prop := | exists_S : forall l, exists_between k l -> exists_between k (S l) | exists_le : forall l, k <= l -> Q l -> exists_between k (S l). diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index de113df6a..ca02c983d 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -119,6 +119,8 @@ CAMLPKGS ?= # Option for making timing files TIMING?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -334,7 +336,7 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: print-pretty-timed:: $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) ifeq (,$(BEFORE)) print-pretty-single-time-diff:: @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' @@ -346,7 +348,7 @@ print-pretty-single-time-diff:: $(HIDE)false else print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index a5a5fa8fe..0d24332f1 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -10,6 +10,20 @@ STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?') STRIP_REP = r'\1' INFINITY = '\xe2\x88\x9e' +def parse_args(argv, USAGE, HELP_STRING): + sort_by = 'auto' + if any(arg.startswith('--sort-by=') for arg in argv[1:]): + sort_by = [arg for arg in argv[1:] if arg.startswith('--sort-by=')][-1][len('--sort-by='):] + args = [arg for arg in argv if not arg.startswith('--sort-by=')] + if len(args) < 3 or '--help' in args[1:] or '-h' in args[1:] or sort_by not in ('auto', 'absolute', 'diff'): + print(USAGE) + if '--help' in args[1:] or '-h' in args[1:]: + print(HELP_STRING) + if len(args) == 2: sys.exit(0) + sys.exit(1) + return sort_by, args + + def reformat_time_string(time): seconds, milliseconds = time.split('.') seconds = int(seconds) @@ -108,6 +122,7 @@ def format_percentage(num, signed=True): return sign + '%d.%02d%%' % (whole_part, frac_part) def make_diff_table_string(left_times_dict, right_times_dict, + sort_by='auto', descending=True, left_tag="After", tag="File Name", right_tag="Before", with_percent=True, change_tag="Change", percent_change_tag="% Change"): @@ -125,10 +140,15 @@ def make_diff_table_string(left_times_dict, right_times_dict, if rseconds != 0 else (INFINITY if lseconds > 0 else 'N/A'))) for name, lseconds, rseconds in prediff_times) # update to sort by approximate difference, first - get_key = make_sorting_key(all_names_dict, descending=descending) - all_names_dict = dict((name, (fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending), get_key(name))) - for name in all_names_dict.keys()) - names = sorted(all_names_dict.keys(), key=all_names_dict.get) + get_key_abs = make_sorting_key(all_names_dict, descending=descending) + get_key_diff = (lambda name: fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending)) + if sort_by == 'absolute': + get_key = get_key_abs + elif sort_by == 'diff': + get_key = get_key_diff + else: # sort_by == 'auto' + get_key = (lambda name: (get_key_diff(name), get_key_abs(name))) + names = sorted(all_names_dict.keys(), key=get_key) #names = get_sorted_file_list_from_times_dict(all_names_dict, descending=descending) # set the widths of each of the columns by the longest thing to go in that column left_sum = sum_times(left_times_dict.values()) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index fd4be08b1..2433cb1d0 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -455,7 +455,7 @@ let usage () = eprintf " -coqlib dir : set the coq standard library directory\n"; eprintf " -suffix s : \n"; eprintf " -slash : deprecated, no effect\n"; - eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed"; + eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index 2d33503c3..32c52c7a1 100755 --- a/tools/make-both-single-timing-files.py +++ b/tools/make-both-single-timing-files.py @@ -3,16 +3,10 @@ import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] + USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] HELP_STRING = r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table''' - if len(sys.argv) < 3 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(USAGE) - if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(HELP_STRING) - if len(sys.argv) == 2: sys.exit(0) - sys.exit(1) - else: - left_dict = get_single_file_times(sys.argv[1]) - right_dict = get_single_file_times(sys.argv[2]) - table = make_diff_table_string(left_dict, right_dict, tag="Code") - print_or_write_table(table, sys.argv[3:]) + sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) + left_dict = get_single_file_times(args[1]) + right_dict = get_single_file_times(args[2]) + table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=sort_by) + print_or_write_table(table, args[3:]) diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py index 69ec5a663..f730a8d6b 100755 --- a/tools/make-both-time-files.py +++ b/tools/make-both-time-files.py @@ -3,20 +3,14 @@ import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] + USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] HELP_STRING = r'''Formats timing information from the output of two invocations of `make TIMED=1` into a sorted table. The input is expected to contain lines in the format: FILE_NAME (...user: NUMBER_IN_SECONDS...) ''' - if len(sys.argv) < 3 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(USAGE) - if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(HELP_STRING) - if len(sys.argv) == 2: sys.exit(0) - sys.exit(1) - else: - left_dict = get_times(sys.argv[1]) - right_dict = get_times(sys.argv[2]) - table = make_diff_table_string(left_dict, right_dict) - print_or_write_table(table, sys.argv[3:]) + sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) + left_dict = get_times(args[1]) + right_dict = get_times(args[2]) + table = make_diff_table_string(left_dict, right_dict, sort_by=sort_by) + print_or_write_table(table, args[3:]) diff --git a/vernac/record.ml b/vernac/record.ml index d9dc16d96..1e464eb8b 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -531,6 +531,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari match univs with | Polymorphic_const_entry univs -> let usubst, auctx = Univ.abstract_universes univs in + let usubst = Univ.make_instance_subst usubst in let map c = Vars.subst_univs_level_constr usubst c in let fields = Context.Rel.map map fields in let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in |
