diff options
62 files changed, 474 insertions, 306 deletions
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index c7437c4a4a..a9230042a5 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 27ac0631a7..1e7f982a57 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 0bc43c1104..8f1f1e699b 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. Vernacular Commands diff --git a/INSTALL.ide b/INSTALL.ide index 513e37c91f..26c192baab 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 9a838b85ca..d8474ae131 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/checker/univ.ml b/checker/univ.ml index 4f31318132..7d01657df7 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 0eadc6801f..21c94d9529 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/configure.ml b/configure.ml index a86b78ba5d..e991eadace 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 3dd24bac4d..af2a13a842 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 b446c3e974..6b83579def 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 cfcc09b327..dc33838f1e 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 48f1d3759b..2c2f0fa47c 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/appveyor.bat b/dev/ci/appveyor.bat index 72ee89962c..dec6f0d182 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/doc/debugging.md b/dev/doc/debugging.md index fa145d498a..fd3cbd1bc3 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 80da845174..f48013cf2e 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 4c4dbe1e97..d7acf01f1d 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 0000000000..beb26d9104 --- /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 30039d4898..8f9d876cb8 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 436099e74d..2d98534307 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 ef0f4af8f6..c4c0435c5f 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 991c9745e9..05775bfbe5 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 1d3311edc2..3d4c885b3a 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -555,12 +555,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 dea5626f8e..7a46ac4e68 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 a6a0f5850e..e300401c9f 100644 --- a/doc/refman/coqide.png +++ b/doc/refman/coqide.png diff --git a/engine/evd.ml b/engine/evd.ml index e33c851f6e..0e94721589 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 6131f4c033..6f2b3c4b26 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 30490ec56a..eaddf98a83 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 1a98d969b4..130dcf8bb8 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/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 3ecb3d3212..6e5c0f8515 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 d1b79ffcdd..55f825c251 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 5b4b5f67b8..75bfca3078 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 3105214d5e..ed1cd5276c 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 7b921d35be..23a578d993 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 1f2ae0b6cc..b117f8714b 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 f7e755f005..b7eb481ee3 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/opaqueproof.ml b/kernel/opaqueproof.ml index 45a62d55a1..c2fcfbfd6a 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 20d76ce238..c8339e6eb3 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 2e4426d621..cbc4ee2ec4 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) = diff --git a/kernel/univ.ml b/kernel/univ.ml index 8cf9028fb1..f72f6f26a9 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 4593944395..63bef1b81b 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 eae917b5a2..b3b3eff628 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 964de4e958..b74d25260f 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 499e2ae21f..971089c171 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 721e2896f7..cf75d5f8cf 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 cf51257571..3e3965b94a 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 d59102b6c7..8ac471404a 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 ac88468545..78de0437d0 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 f153b63410..3f947fd23f 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 b41fb4e4dd..8df8f84742 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/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index 07689389ff..706d36e1d5 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 e1bf32f3ce..bc2fea2bd5 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/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 898af5590a..2439d3f378 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 0000000000..94a0b19118 --- /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 0000000000..e566bd7bab --- /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/theories/Arith/Between.v b/theories/Arith/Between.v index 9b40710858..ead08b3ebb 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 de113df6a5..ca02c983d2 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 a5a5fa8fe5..0d24332f1e 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/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index 2d33503c36..32c52c7a17 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 69ec5a6631..f730a8d6bd 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 d9dc16d96e..1e464eb8bf 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 |
