diff options
50 files changed, 689 insertions, 245 deletions
diff --git a/.gitignore b/.gitignore index 760ccc60c3..b665b2f86d 100644 --- a/.gitignore +++ b/.gitignore @@ -64,12 +64,9 @@ plugins/micromega/.micromega.ml.generated kernel/byterun/dllcoqrun.so coqdoc.sty coqdoc.css -time-of-build.log -time-of-build-pretty.log -time-of-build-before.log -time-of-build-after.log -time-of-build-pretty.log2 -time-of-build-pretty.log3 +time-of-build*.log +time-of-build*.log2 +time-of-build*.log3 .csdp.cache test-suite/.lia.cache test-suite/.nra.cache diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 8cff8f66b7..d9adaf5dc7 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -17,8 +17,8 @@ well. - [Writing tutorials and blog posts](#writing-tutorials-and-blog-posts) - [Contributing to the wiki](#contributing-to-the-wiki) - [Creating and maintaining Coq packages](#creating-and-maintaining-coq-packages) - - [Distribution](#distribution) - - [Support](#support) + - [Distribution of Coq packages](#distribution-of-coq-packages) + - [Support for plugin and library authors](#support-for-plugin-and-library-authors) - [Standard libraries](#standard-libraries) - [Maintaining existing packages in coq-community](#maintaining-existing-packages-in-coq-community) - [Contributing to the editor support packages](#contributing-to-the-editor-support-packages) @@ -161,14 +161,14 @@ tools is great so that others can start building new things on top. Having an extensive and healthy package ecosystem will be key to the success of Coq. -#### Distribution #### +#### Distribution of Coq packages #### You can distribute your library or plugin through the [Coq package index][Coq-package-index]. Tools can be advertised on the [tools page][tools-website] of the Coq website, or the [tools page][tools-wiki] of the wiki. -#### Support #### +#### Support for plugin and library authors #### You can find advice and best practices about maintaining a Coq project on the [coq-community wiki][coq-community-wiki]. @@ -529,10 +529,20 @@ how you can anticipate the results of the CI before opening a PR. Such a failure can indicate either a bug in your branch, or a breaking change that you introduced voluntarily. All such breaking changes should be properly documented in the [user changelog][user-changelog]. -Furthermore, a backward-compatible fix should be found, and this fix -should be merged in the broken projects *before* your PR to the Coq -repository can be. You can use the same documentation as above to -learn about testing and fixing locally the broken libraries. +Furthermore, a backward-compatible fix should be found, properly +documented in the changelog when non-obvious, and this fix should be +merged in the broken projects *before* your PR to the Coq repository +can be. + +Note that once the breaking change is well understood, it should not +feel like it is your role to fix every project that is affected: as +long as reviewers have approved and are ready to integrate your +breaking change, you are entitled to (politely) request project +authors / maintainers to fix the breakage on their own, or help you +fix it. Obviously, you should leave enough time for this to happen +(you cannot expect a project maintainer to allocate time for this as +soon as you request it) and you should be ready to listen to more +feedback and reconsider the impact of your change. #### Understanding reviewers' feedback #### diff --git a/Makefile.build b/Makefile.build index 8a11d913a9..6590f5f308 100644 --- a/Makefile.build +++ b/Makefile.build @@ -50,6 +50,12 @@ VALIDATE ?= # When non-empty, passed as extra arguments to coqtop/coqc: COQUSERFLAGS ?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto +# Option for changing the fuzz parameter on the output file +TIMING_FUZZ ?= 0 +# Option for changing whether to use real or user time for timing tables +TIMING_REAL?= # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -104,6 +110,19 @@ include Makefile.dev ## provides the 'printers' and 'revision' rules ########################################################################### # Timing targets ########################################################################### +ifeq (0,$(TIMING_REAL)) +TIMING_REAL_ARG := +TIMING_USER_ARG := --user +else +ifeq (1,$(TIMING_REAL)) +TIMING_REAL_ARG := --real +TIMING_USER_ARG := +else +TIMING_REAL_ARG := +TIMING_USER_ARG := +endif +endif + make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: @@ -111,21 +130,21 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: $(HIDE)($(MAKE) --no-print-directory $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed print-pretty-timed:: - $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_REAL_ARG) $(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) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_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' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' $(HIDE)false else ifeq (,$(AFTER)) 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' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' $(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) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: @@ -858,7 +877,7 @@ endif $(HIDE)$(BOOTCOQC) $< -vio -noglob %.v.timing.diff: %.v.before-timing %.v.after-timing - $(SHOW)PYTHON TIMING-DIFF $< + $(SHOW)'PYTHON TIMING-DIFF $*.v.{before,after}-timing' $(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" diff --git a/Makefile.dev b/Makefile.dev index b1e142333a..6e9b5356ab 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -140,17 +140,17 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ ### 4) plugins ################ -OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO)) -MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) -RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) -NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) -FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO)) -BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO)) -RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO)) -EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO)) +OMEGAVO:=$(filter theories/omega/%, $(THEORIESVO)) +MICROMEGAVO:=$(filter theories/micromega/%, $(THEORIESVO)) +RINGVO:=$(filter theories/setoid_ring/%, $(THEORIESVO)) +NSATZVO:=$(filter theories/nsatz/%, $(THEORIESVO)) +FUNINDVO:=$(filter theories/funind/%, $(THEORIESVO)) +BTAUTOVO:=$(filter theories/btauto/%, $(THEORIESVO)) +RTAUTOVO:=$(filter theories/rtauto/%, $(THEORIESVO)) +EXTRACTIONVO:=$(filter theories/extraction/%, $(THEORIESVO)) CCVO:= -DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO)) -LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO)) +DERIVEVO:=$(filter theories/derive/%, $(THEORIESVO)) +LTACVO:=$(filter theories/ltac/%, $(THEORIESVO)) omega: $(OMEGAVO) $(OMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 9ed7180807..6a740b9033 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -43,9 +43,10 @@ See also [`test-suite/README.md`](../../test-suite/README.md) for information ab ### Breaking changes When your PR breaks an external project we test in our CI, you must -prepare a patch (or ask someone to prepare a patch) to fix the -project. There is experimental support for an improved workflow, see -[the next section](#experimental-automatic-overlay-creation-and-building), below +prepare a patch (or ask someone—possibly the project author—to +prepare a patch) to fix the project. There is experimental support for +an improved workflow, see [the next +section](#experimental-automatic-overlay-creation-and-building), below are the steps to manually prepare a patch: 1. Fork the external project, create a new branch, push a commit adapting diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index 06b617d4c1..6649820f22 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -1,36 +1,40 @@ Information for external library / Coq plugin authors ----------------------------------------------------- -You are encouraged to consider submitting your development for addition to +You are encouraged to consider submitting your project for addition to Coq's CI. This means that: -- Any time that a proposed change is breaking your development, Coq developers - will send you patches to adapt it or, at the very least, will work with you - to see how to adapt it. +- Any time that a proposed change is breaking your project, Coq + developers and contributors will send you patches to adapt it or + will explain how to adapt it and work with you to ensure that you + manage to do it. On the condition that: -- At the time of the submission, your development works with Coq's +- At the time of the submission, your project works with Coq's `master` branch. -- Your development is publicly available in a git repository and we can easily +- Your project is publicly available in a git repository and we can easily send patches to you (e.g. through pull / merge requests). - You react in a timely manner to discuss / integrate those patches. + When seeking your help for preparing such patches, we will accept + that it takes longer than when we are just requesting to integrate a + simple (and already fully prepared) patch. - You do not push, to the branches that we test, commits that haven't been first tested to compile with the corresponding branch(es) of Coq. - For that, we recommend setting a CI system for you development, see + For that, we recommend setting a CI system for you project, see [supported CI images for Coq](#supported-ci-images-for-coq) below. -- You maintain a reasonable build time for your development, or you provide +- You maintain a reasonable build time for your project, or you provide a "lite" target that we can use. In case you forget to comply with these last three conditions, we would reach -out to you and give you a 30-day grace period during which your development +out to you and give you a 30-day grace period during which your project would be moved into our "allow failure" category. At the end of the grace -period, in the absence of progress, the development would be removed from our +period, in the absence of progress, the project would be removed from our CI. ### Timely merging of overlays @@ -47,7 +51,7 @@ these kind of merges. ### OCaml and plugin-specific considerations -Developments that link against Coq's OCaml API [most of them are known +Projects that link against Coq's OCaml API [most of them are known as "plugins"] do have some special requirements: - Coq's OCaml API is not stable. We hope to improve this in the future @@ -65,7 +69,7 @@ as "plugins"] do have some special requirements: uses. In particular, warnings that are considered fatal by the Coq developers _must_ be also fatal for plugin CI code. -### Add your development by submitting a pull request +### Add your project by submitting a pull request Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the @@ -75,7 +79,7 @@ Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an example. **Do not hesitate to submit an incomplete pull request if you need help to finish it.** -You may also be interested in having your development tested in our +You may also be interested in having your project tested in our performance benchmark. Currently this is done by providing an OPAM package in https://github.com/coq/opam-coq-archive and opening an issue at https://github.com/coq/coq-bench/issues. @@ -83,13 +87,13 @@ https://github.com/coq/coq-bench/issues. ### Recommended branching policy. It is sometimes the case that you will need to maintain a branch of -your development for particular Coq versions. This is in fact very -likely if your development includes a Coq ML plugin. +your project for particular Coq versions. This is in fact very likely +if your project includes a Coq ML plugin. -We thus recommend a branching convention that mirrors Coq's branching -policy. Then, you would have a `master` branch that follows Coq's -`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so -on. +For such projects, we recommend a branching convention that mirrors +Coq's branching policy. Then, you would have a `master` branch that +follows Coq's `master`, a `v8.8` branch that works with Coq's `v8.8` +branch and so on. This convention will be supported by tools in the future to make some developer commands work more seamlessly. diff --git a/dev/doc/INSTALL.make.md b/dev/doc/INSTALL.make.md index 3db5d0b14f..f81630c55d 100644 --- a/dev/doc/INSTALL.make.md +++ b/dev/doc/INSTALL.make.md @@ -102,6 +102,14 @@ Detailed Installation Procedure. it is recommended to compile in parallel, via make -jN where N is your number of cores. + If you wish to create timing logs for the standard library, you can + pass `TIMING=1` (for per-line timing files) or `TIMED=1` (for + per-file timing on stdout). Further variables and targets are + available for more detailed timing analysis; see the section of the + reference manual on `coq_makefile`. If there is any timing target + or variable supported by `coq_makefile`-made Makefiles which is not + supported by Coq's own Makefile, please report that as a bug. + 5. You can now install the Coq system. Executables, libraries, and manual pages are copied in some standard places of your system, defined at configuration time (step 3). Just do diff --git a/doc/changelog/02-specification-language/11600-uniform-syntax.rst b/doc/changelog/02-specification-language/11600-uniform-syntax.rst new file mode 100644 index 0000000000..3fa3f80301 --- /dev/null +++ b/doc/changelog/02-specification-language/11600-uniform-syntax.rst @@ -0,0 +1,4 @@ +- **Added:** + New syntax :g:`Inductive Acc A R | x : Prop := ...` to specify which + parameters of an inductive are uniform. + (`#11600 <https://github.com/coq/coq/pull/11600>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/08-tools/11302-better-timing-scripts-options.rst b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst new file mode 100644 index 0000000000..3b20bbf75d --- /dev/null +++ b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst @@ -0,0 +1,35 @@ +- **Added:** + The ``make-both-single-timing-files.py`` script now accepts a + ``--fuzz=N`` parameter on the command line which determines how many + characters two lines may be offset in the "before" and "after" + timing logs while still being considered the same line. When + invoking this script via the ``print-pretty-single-time-diff`` + target in a ``Makefile`` made by ``coq_makefile``, you can set this + argument by passing ``TIMING_FUZZ=N`` to ``make`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). + +- **Added:** + The ``make-one-time-file.py`` and ``make-both-time-files.py`` + scripts now accept a ``--real`` parameter on the command line to + print real times rather than user times in the tables. The + ``make-both-single-timing-files.py`` script accepts a ``--user`` + parameter to use user times. When invoking these scripts via the + ``print-pretty-timed`` or ``print-pretty-timed-diff`` or + ``print-pretty-single-time-diff`` targets in a ``Makefile`` made by + ``coq_makefile``, you can set this argument by passing + ``TIMING_REAL=1`` (to pass ``--real``) or ``TIMING_REAL=0`` (to pass + ``--user``) to ``make`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). + +- **Added:** + Coq's build system now supports both ``TIMING_FUZZ``, + ``TIMING_SORT_BY``, and ``TIMING_REAL`` just like a ``Makefile`` + made by ``coq_makefile`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). + +- **Fixed:** + The various timing targets for Coq's standard library now correctly + display and label the "before" and "after" columns, rather than + mixing them up (`#11302 <https://github.com/coq/coq/pull/11302>`_ + fixes `#11301 <https://github.com/coq/coq/issues/11301>`_, by Jason + Gross). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 721c7a7a51..7ce4538a4d 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1063,8 +1063,17 @@ Parameterized inductive types | cons3 : A -> list3 -> list3. End list3. - Attributes ``uniform`` and ``nonuniform`` respectively enable and - disable uniform parameters for a single inductive declaration block. + For finer control, you can use a ``|`` between the uniform and + the non-uniform parameters: + + .. coqtop:: in reset + + Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop + := Acc_in : (forall y, R y x -> Acc y) -> Acc x. + + The flag can then be seen as deciding whether the ``|`` is at the + beginning (when the flag is unset) or at the end (when it is set) + of the parameters when not explicitly given. .. seealso:: Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 3d1fc6d4b9..179dff9959 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -255,14 +255,20 @@ file timing data: one, you can pass them via the variable ``TGTS``, e.g., ``make pretty-timed TGTS="a.vo b.vo"``. - .. :: + .. note:: This target requires ``python`` to build the table. .. note:: This target will *append* to the timing log; if you want a - fresh start, you must remove the ``filetime-of-build.log`` or + fresh start, you must remove the file ``time-of-build.log`` or ``run make cleanall``. + .. note:: + By default the table displays user times. If the build log + contains real times (which it does by default), passing + ``TIMING_REAL=1`` to ``make pretty-timed`` will use real times + rather than user times in the table. + .. example:: For example, the output of ``make pretty-timed`` may look like this: @@ -310,6 +316,15 @@ file timing data: (which are frequently noise); lexicographic sorting forces an order on files which take effectively no time to compile. + If you prefer a different sorting order, you can pass + ``TIMING_SORT_BY=absolute`` to sort by the total time taken, or + ``TIMING_SORT_BY=diff`` to sort by the signed difference in + time. + + .. note:: + Just like ``pretty-timed``, this table defaults to using user + times. Pass ``TIMING_REAL=1`` to ``make`` on the command line to show real times instead. + .. example:: For example, the output table from @@ -349,7 +364,7 @@ line timing data: :: - print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing + print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing this target will make a sorted table of the per-line timing differences between the timing logs in the ``BEFORE`` and ``AFTER`` files, display it, and @@ -364,6 +379,28 @@ line timing data: .. note:: This target requires python to build the table. + .. note:: + This target follows the same sorting order as the + ``print-pretty-timed-diff`` target, and supports the same + options for the ``TIMING_SORT_BY`` variable. + + .. note:: + By default, two lines are only considered the same if the + character offsets and initial code strings are identical. Passing + ``TIMING_FUZZ=N`` relaxes this constraint by allowing the + character locations to differ by up to ``N``, as long + as the total number of characters and initial code strings + continue to match. This is useful when there are small changes + to a file, and you want to match later lines that have not + changed even though the character offsets have changed. + + .. note:: + By default the table picks up real times, under the assumption + that when comparing line-by-line, the real time is a more + accurate representation as it includes disk time and time spent + in the native compiler. Passing ``TIMING_REAL=0`` to ``make`` + will use user times rather than real times in the table. + .. example:: For example, running ``print-pretty-single-time-diff`` might give a table like this: diff --git a/ide/coq.ml b/ide/coq.ml index 4d6ba55d76..0c6aef0305 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -133,10 +133,10 @@ and asks_for_coqtop args = ~filter:false ~filename:(coqtop_path ()) () in match file with - | Some _ -> - let () = custom_coqtop := file in + | [file] -> + let () = custom_coqtop := Some file in filter_coq_opts args - | None -> exit 0 + | _ -> exit 0 exception WrongExitStatus of string diff --git a/ide/coqide.ml b/ide/coqide.ml index ccf6d40b2b..143a12deeb 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -282,9 +282,8 @@ let load ?parent _ = let filename = try notebook#current_term.fileops#filename with Invalid_argument _ -> None in - match select_file_for_open ~title:"Load file" ?parent ?filename () with - | None -> () - | Some f -> FileAux.load_file f + let filenames = select_file_for_open ~title:"Load file" ~multiple:true ?parent ?filename () in + List.iter FileAux.load_file filenames let save ?parent _ = on_current_term (FileAux.check_save ?parent ~saveas:false) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 1cf065cf25..38da229d61 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -259,7 +259,7 @@ let current_dir () = match project_path#get with | None -> "" | Some dir -> dir -let select_file_for_open ~title ?(filter=true) ?parent ?filename () = +let select_file_for_open ~title ?(filter=true) ?(multiple=false) ?parent ?filename () = let file_chooser = GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title ?parent () in @@ -271,6 +271,7 @@ let select_file_for_open ~title ?(filter=true) ?parent ?filename () = file_chooser#add_filter (filter_all_files ()) end; file_chooser#set_default_response `OPEN; + file_chooser#set_select_multiple multiple; let dir = match filename with | None -> current_dir () | Some f -> Filename.dirname f in @@ -279,12 +280,12 @@ let select_file_for_open ~title ?(filter=true) ?parent ?filename () = match file_chooser#run () with | `OPEN -> begin - match file_chooser#filename with - | None -> None - | Some _ as f -> - project_path#set file_chooser#current_folder; f + let filenames = file_chooser#get_filenames in + (if filenames <> [] then + project_path#set file_chooser#current_folder); + filenames end - | `DELETE_EVENT | `CANCEL -> None in + | `DELETE_EVENT | `CANCEL -> [] in file_chooser#destroy (); file diff --git a/ide/ideutils.mli b/ide/ideutils.mli index bacb273657..af30cd2b05 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -31,7 +31,7 @@ val find_tag_start : GText.tag -> GText.iter -> GText.iter val find_tag_stop : GText.tag -> GText.iter -> GText.iter val select_file_for_open : - title:string -> ?filter:bool -> ?parent:GWindow.window -> ?filename:string -> unit -> string option + title:string -> ?filter:bool -> ?multiple:bool -> ?parent:GWindow.window -> ?filename:string -> unit -> string list val select_file_for_save : title:string -> ?parent:GWindow.window -> ?filename:string -> unit -> string option val try_convert : string -> string diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 06232b8e1a..c198c4eb9b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -792,11 +792,9 @@ let rec flatten_application c = match DAst.get c with let extern_possible_prim_token (custom,scopes) r = let (sc,n) = uninterp_prim_token r in - let coercion = - if entry_has_prim_token n custom then [] else - match availability_of_entry_coercion custom InConstrEntrySomeLevel with - | None -> raise No_match - | Some coercion -> coercion in + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> match availability_of_prim_token n sc scopes with | None -> raise No_match | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) diff --git a/interp/notation.ml b/interp/notation.ml index 9d6cab550d..93969f3718 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1349,34 +1349,6 @@ let entry_has_ident = function | InCustomEntryLevel (s,n) -> try String.Map.find s !entry_has_ident_map <= n with Not_found -> false -let entry_has_numeral_map = ref String.Map.empty -let entry_has_string_map = ref String.Map.empty - -let declare_custom_entry_has_numeral s n = - try - let p = String.Map.find s !entry_has_numeral_map in - user_err (str "Custom entry " ++ str s ++ - str " has already a rule for numerals at level " ++ int p ++ str ".") - with Not_found -> - entry_has_numeral_map := String.Map.add s n !entry_has_numeral_map - -let declare_custom_entry_has_string s n = - try - let p = String.Map.find s !entry_has_string_map in - user_err (str "Custom entry " ++ str s ++ - str " has already a rule for strings at level " ++ int p ++ str ".") - with Not_found -> - entry_has_string_map := String.Map.add s n !entry_has_string_map - -let entry_has_prim_token prim = function - | InConstrEntrySomeLevel -> true - | InCustomEntryLevel (s,n) -> - match prim with - | Numeral _ -> - (try String.Map.find s !entry_has_numeral_map <= n with Not_found -> false) - | String _ -> - (try String.Map.find s !entry_has_string_map <= n with Not_found -> false) - let uninterp_prim_token c = match glob_prim_constr_key c with | None -> raise Notation_ops.No_match diff --git a/interp/notation.mli b/interp/notation.mli index 707be6cb87..ea5125f7ec 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -305,12 +305,9 @@ val availability_of_entry_coercion : notation_entry_level -> notation_entry_leve val declare_custom_entry_has_global : string -> int -> unit val declare_custom_entry_has_ident : string -> int -> unit -val declare_custom_entry_has_numeral : string -> int -> unit -val declare_custom_entry_has_string : string -> int -> unit val entry_has_global : notation_entry_level -> bool val entry_has_ident : notation_entry_level -> bool -val entry_has_prim_token : prim_token -> notation_entry_level -> bool (** Rem: printing rules for primitive token are canonical *) diff --git a/parsing/extend.ml b/parsing/extend.ml index 178f7354f2..848861238a 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -29,7 +29,6 @@ type 'a constr_entry_key_gen = | ETIdent | ETGlobal | ETBigint - | ETString | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *) @@ -54,7 +53,6 @@ type constr_prod_entry_key = | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) - | ETProdString (* Parsed as a string *) | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *) | ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *) | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *) diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml index 5c220abeda..a5ade43295 100644 --- a/parsing/notgram_ops.ml +++ b/parsing/notgram_ops.ml @@ -55,12 +55,11 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with | ETIdent, ETIdent -> true | ETGlobal, ETGlobal -> true | ETBigint, ETBigint -> true -| ETString, ETString -> true | ETBinder b1, ETBinder b2 -> b1 == b2 | ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) -> notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2 | ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 -| (ETIdent | ETGlobal | ETBigint | ETString | ETBinder _ | ETConstr _ | ETPattern _), _ -> false +| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) = let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index fdbad2ab9e..c7dfe69fb1 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1476,7 +1476,7 @@ let do_build_inductive in let rel_ind i ext_rel_constructors = ((CAst.make @@ relnames.(i)), - rel_params, + (rel_params,None), Some rel_arities.(i), ext_rel_constructors),[] in diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh index 4a50759bdb..a6f35db17c 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh @@ -5,6 +5,10 @@ set -e cd "$(dirname "${BASH_SOURCE[0]}")" -"$COQLIB"/tools/make-both-time-files.py time-of-build-after.log.in time-of-build-before.log.in time-of-build-both.log +"$COQLIB"/tools/make-both-time-files.py time-of-build-after.log.in time-of-build-before.log.in time-of-build-both-user.log -diff -u time-of-build-both.log.expected time-of-build-both.log || exit $? +diff -u time-of-build-both-user.log.expected time-of-build-both-user.log || exit $? + +"$COQLIB"/tools/make-both-time-files.py --real time-of-build-after.log.in time-of-build-before.log.in time-of-build-both-real.log + +diff -u time-of-build-both-real.log.expected time-of-build-both-real.log || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected new file mode 100644 index 0000000000..ea600b000e --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected @@ -0,0 +1,26 @@ +After | File Name | Before || Change | % Change +---------------------------------------------------------------------------------------------- +20m46.07s | Total | 23m06.30s || -2m20.23s | -10.11% +---------------------------------------------------------------------------------------------- +4m16.77s | Specific/X25519/C64/ladderstep | 5m16.83s || -1m00.06s | -18.95% +3m01.77s | Specific/solinas32_2e255m765_13limbs/femul | 3m27.94s || -0m26.16s | -12.58% +2m35.79s | Specific/solinas32_2e255m765_12limbs/femul | 2m59.21s || -0m23.42s | -13.06% +3m22.96s | Specific/NISTP256/AMD64/femul | 3m37.80s || -0m14.84s | -6.81% +0m39.72s | Specific/X25519/C64/femul | 0m42.98s || -0m03.25s | -7.58% +0m38.19s | Specific/NISTP256/AMD64/feadd | 0m40.48s || -0m02.28s | -5.65% +0m34.35s | Specific/X25519/C64/freeze | 0m36.42s || -0m02.07s | -5.68% +0m33.08s | Specific/X25519/C64/fesquare | 0m35.23s || -0m02.14s | -6.10% +0m31.00s | Specific/NISTP256/AMD64/feopp | 0m32.08s || -0m01.07s | -3.36% +0m27.81s | Specific/NISTP256/AMD64/fenz | 0m28.91s || -0m01.10s | -3.80% +0m27.11s | Specific/X25519/C64/fecarry | 0m28.85s || -0m01.74s | -6.03% +0m24.71s | Specific/X25519/C64/fesub | 0m26.11s || -0m01.39s | -5.36% +0m49.44s | Specific/solinas32_2e255m765_13limbs/Synthesis | 0m49.50s || -0m00.06s | -0.12% +0m43.34s | Specific/NISTP256/AMD64/fesub | 0m43.78s || -0m00.43s | -1.00% +0m40.13s | Specific/solinas32_2e255m765_12limbs/Synthesis | 0m39.53s || +0m00.60s | +1.51% +0m22.81s | Specific/X25519/C64/feadd | 0m23.43s || -0m00.62s | -2.64% +0m13.45s | Specific/NISTP256/AMD64/Synthesis | 0m13.74s || -0m00.29s | -2.11% +0m11.15s | Specific/X25519/C64/Synthesis | 0m11.23s || -0m00.08s | -0.71% +0m07.33s | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s || -0m00.07s | -0.94% +0m01.93s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s || +0m00.19s | +11.56% +0m01.85s | Specific/Framework/SynthesisFramework | 0m01.95s || -0m00.09s | -5.12% +0m01.38s | Compilers/Z/Bounds/Pipeline | 0m01.18s || +0m00.19s | +16.94%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected index 159e645512..159e645512 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh index 4f39b3ce7e..d4614749e7 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh @@ -5,6 +5,10 @@ set -e cd "$(dirname "${BASH_SOURCE[0]}")" -"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log +"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty-user.log -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $? +diff -u time-of-build-pretty-user.log.expected time-of-build-pretty-user.log || exit $? + +"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty-real.log + +diff -u time-of-build-pretty-real.log.expected time-of-build-pretty-real.log || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected index b9739ddb1d..b9739ddb1d 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected new file mode 100644 index 0000000000..b9739ddb1d --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected @@ -0,0 +1,26 @@ +Time | File Name +---------------------------------------------------------- +19m16.04s | Total +---------------------------------------------------------- +4m01.34s | Specific/X25519/C64/ladderstep +3m09.62s | Specific/NISTP256/AMD64/femul +2m48.52s | Specific/solinas32_2e255m765_13limbs/femul +2m23.70s | Specific/solinas32_2e255m765_12limbs/femul +0m45.75s | Specific/solinas32_2e255m765_13limbs/Synthesis +0m39.59s | Specific/NISTP256/AMD64/fesub +0m36.92s | Specific/solinas32_2e255m765_12limbs/Synthesis +0m36.32s | Specific/X25519/C64/femul +0m35.40s | Specific/NISTP256/AMD64/feadd +0m31.50s | Specific/X25519/C64/freeze +0m30.13s | Specific/X25519/C64/fesquare +0m28.51s | Specific/NISTP256/AMD64/feopp +0m25.50s | Specific/NISTP256/AMD64/fenz +0m24.99s | Specific/X25519/C64/fecarry +0m22.65s | Specific/X25519/C64/fesub +0m20.93s | Specific/X25519/C64/feadd +0m12.55s | Specific/NISTP256/AMD64/Synthesis +0m10.37s | Specific/X25519/C64/Synthesis +0m07.18s | Compilers/Z/Bounds/Pipeline/Definition +0m01.72s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics +0m01.67s | Specific/Framework/SynthesisFramework +0m01.19s | Compilers/Z/Bounds/Pipeline
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected new file mode 100644 index 0000000000..726c19a2e2 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected @@ -0,0 +1,29 @@ +After | Code | Before || Change | % Change +----------------------------------------------------------------------------------------------------------- +0m01.23s | Total | 0m01.28s || -0m00.04s | -3.50% +----------------------------------------------------------------------------------------------------------- +0m00.53s | Chars 260-284 ~ 280-304 [(vm_compute;~reflexivity).] | 0m00.566s || -0m00.03s | -6.36% +0m00.4s | Chars 285-289 ~ 305-309 [Qed.] | 0m00.411s || -0m00.01s | -2.67% +0m00.194s | Chars 031-064 ~ 031-064 [Require~Import~Coq.ZArith.ZArith.] | 0m00.192s || +0m00.00s | +1.04% +0m00.114s | Chars 000-030 ~ 000-030 [Require~Import~Coq.Lists.List.] | 0m00.114s || +0m00.00s | +0.00% +0m00.s | Chars 065-075 ~ 065-075 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 078-086 ~ 078-086 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 078-090 ~ 078-090 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 087-091 ~ 091-095 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 092-102 ~ 096-106 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 105-113 ~ 109-117 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 105-117 ~ 109-121 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 114-118 ~ 122-126 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 119-129 ~ 127-137 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 132-140 ~ 140-148 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 132-144 ~ 140-152 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 141-145 ~ 153-157 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 146-156 ~ 158-168 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 159-167 ~ 171-179 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 159-171 ~ 171-183 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 168-172 ~ 184-188 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 173-183 ~ 189-199 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 186-194 ~ 202-210 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 186-198 ~ 202-214 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 195-199 ~ 215-219 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 200-257 ~ 220-277 [Goal~_~List.repeat~Z.div_eucl~...] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected new file mode 100644 index 0000000000..f6be1d936d --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected @@ -0,0 +1,29 @@ +After | Code | Before || Change | % Change +----------------------------------------------------------------------------------------------------------- +0m01.14s | Total | 0m01.15s || -0m00.00s | -0.77% +----------------------------------------------------------------------------------------------------------- +0m00.504s | Chars 260-284 ~ 280-304 [(vm_compute;~reflexivity).] | 0m00.528s || -0m00.02s | -4.54% +0m00.384s | Chars 285-289 ~ 305-309 [Qed.] | 0m00.4s || -0m00.01s | -4.00% +0m00.172s | Chars 031-064 ~ 031-064 [Require~Import~Coq.ZArith.ZArith.] | 0m00.156s || +0m00.01s | +10.25% +0m00.083s | Chars 000-030 ~ 000-030 [Require~Import~Coq.Lists.List.] | 0m00.072s || +0m00.01s | +15.27% +0m00.004s | Chars 200-257 ~ 220-277 [Goal~_~List.repeat~Z.div_eucl~...] | 0m00.s || +0m00.00s | ∞ +0m00.s | Chars 065-075 ~ 065-075 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 078-086 ~ 078-086 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 078-090 ~ 078-090 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 087-091 ~ 091-095 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 092-102 ~ 096-106 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 105-113 ~ 109-117 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 105-117 ~ 109-121 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 114-118 ~ 122-126 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 119-129 ~ 127-137 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 132-140 ~ 140-148 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 132-144 ~ 140-152 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 141-145 ~ 153-157 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 146-156 ~ 158-168 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 159-167 ~ 171-179 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 159-171 ~ 171-183 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 168-172 ~ 184-188 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 173-183 ~ 189-199 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 186-194 ~ 202-210 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 186-198 ~ 202-214 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 195-199 ~ 215-219 [Qed.] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.after-timing.in b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.after-timing.in new file mode 100644 index 0000000000..c58e7d82d1 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.after-timing.in @@ -0,0 +1,20 @@ +Chars 0 - 30 [Require~Import~Coq.Lists.List.] 0.114 secs (0.083u,0.032s) +Chars 31 - 64 [Require~Import~Coq.ZArith.ZArith.] 0.194 secs (0.172u,0.023s) +Chars 65 - 75 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 78 - 86 [exact~I.] 0. secs (0.u,0.s) +Chars 87 - 91 [Qed.] 0. secs (0.u,0.s) +Chars 92 - 102 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 105 - 113 [exact~I.] 0. secs (0.u,0.s) +Chars 114 - 118 [Qed.] 0. secs (0.u,0.s) +Chars 119 - 129 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 132 - 140 [exact~I.] 0. secs (0.u,0.s) +Chars 141 - 145 [Qed.] 0. secs (0.u,0.s) +Chars 146 - 156 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 159 - 167 [exact~I.] 0. secs (0.u,0.s) +Chars 168 - 172 [Qed.] 0. secs (0.u,0.s) +Chars 173 - 183 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 186 - 194 [exact~I.] 0. secs (0.u,0.s) +Chars 195 - 199 [Qed.] 0. secs (0.u,0.s) +Chars 200 - 257 [Goal~_~List.repeat~Z.div_eucl~...] 0. secs (0.004u,0.s) +Chars 260 - 284 [(vm_compute;~reflexivity).] 0.53 secs (0.504u,0.024s) +Chars 285 - 289 [Qed.] 0.4 secs (0.384u,0.016s) diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in new file mode 100644 index 0000000000..b49c1b1cb7 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in @@ -0,0 +1,20 @@ +Chars 0 - 30 [Require~Import~Coq.Lists.List.] 0.114 secs (0.072u,0.044s) +Chars 31 - 64 [Require~Import~Coq.ZArith.ZArith.] 0.192 secs (0.156u,0.035s) +Chars 65 - 75 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 78 - 90 [constructor.] 0. secs (0.u,0.s) +Chars 91 - 95 [Qed.] 0. secs (0.u,0.s) +Chars 96 - 106 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 109 - 121 [constructor.] 0. secs (0.u,0.s) +Chars 122 - 126 [Qed.] 0. secs (0.u,0.s) +Chars 127 - 137 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 140 - 152 [constructor.] 0. secs (0.u,0.004s) +Chars 153 - 157 [Qed.] 0. secs (0.u,0.s) +Chars 158 - 168 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 171 - 183 [constructor.] 0. secs (0.u,0.s) +Chars 184 - 188 [Qed.] 0. secs (0.u,0.s) +Chars 189 - 199 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 202 - 214 [constructor.] 0. secs (0.u,0.s) +Chars 215 - 219 [Qed.] 0. secs (0.u,0.s) +Chars 220 - 277 [Goal~_~List.repeat~Z.div_eucl~...] 0. secs (0.u,0.s) +Chars 280 - 304 [(vm_compute;~reflexivity).] 0.566 secs (0.528u,0.039s) +Chars 305 - 309 [Qed.] 0.411 secs (0.4u,0.008s) diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v new file mode 100644 index 0000000000..7141065b52 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v @@ -0,0 +1,20 @@ +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +Goal True. + exact I. +Qed. +Goal True. + exact I. +Qed. +Goal True. + exact I. +Qed. +Goal True. + exact I. +Qed. +Goal True. + exact I. +Qed. +Goal List.repeat Z.div_eucl 5 = List.repeat Z.div_eucl 5. + vm_compute; reflexivity. +Qed. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.v b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.v new file mode 100644 index 0000000000..e152689ee4 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.v @@ -0,0 +1,20 @@ +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +Goal True. + constructor. +Qed. +Goal True. + constructor. +Qed. +Goal True. + constructor. +Qed. +Goal True. + constructor. +Qed. +Goal True. + constructor. +Qed. +Goal List.repeat Z.div_eucl 5 = List.repeat Z.div_eucl 5. + vm_compute; reflexivity. +Qed. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh new file mode 100755 index 0000000000..980bf9cf01 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh @@ -0,0 +1,14 @@ +#!/usr/bin/env bash + +set -x +set -e + +cd "$(dirname "${BASH_SOURCE[0]}")" + +"$COQLIB"/tools/make-both-single-timing-files.py --fuzz=20 foo.v.after-timing.in foo.v.before-timing.in foo-real.v.timing.diff || exit $? + +diff -u foo-real.v.timing.diff.expected foo-real.v.timing.diff || exit $? + +"$COQLIB"/tools/make-both-single-timing-files.py --fuzz=20 --user foo.v.after-timing.in foo.v.before-timing.in foo-user.v.timing.diff || exit $? + +diff -u foo-user.v.timing.diff.expected foo-user.v.timing.diff || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh index cfacf738a3..4b5acb9168 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh @@ -10,3 +10,4 @@ export COQLIB ./001-correct-diff-sorting-order/run.sh ./002-single-file-sorting/run.sh ./003-non-utf8/run.sh +./004-per-file-fuzz/run.sh diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 1c8f237bb8..807914a671 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -14,8 +14,6 @@ Entry constr:myconstr is : nat [<< # 0 >>] : option nat -[2 + 3] - : nat [1 {f 1}] : Expr fun (x : nat) (y z : Expr) => [1 + y z + {f x}] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4ab800c9ba..2906698386 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -22,9 +22,6 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9). Check [ << # 0 >> ]. -Notation "n" := n%nat (in custom myconstr at level 0, n bigint). -Check [ 2 + 3 ]. - End A. Module B. diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v index 651247937d..e2b4694fff 100644 --- a/test-suite/success/uniform_inductive_parameters.v +++ b/test-suite/success/uniform_inductive_parameters.v @@ -1,23 +1,22 @@ -Module Att. - #[uniform] Inductive list (A : Type) := - | nil : list - | cons : A -> list -> list. - Check (list : Type -> Type). - Check (cons : forall A, A -> list A -> list A). -End Att. - Set Uniform Inductive Parameters. Inductive list (A : Type) := -| nil : list -| cons : A -> list -> list. + | nil : list + | cons : A -> list -> list. Check (list : Type -> Type). Check (cons : forall A, A -> list A -> list A). Inductive list2 (A : Type) (A' := prod A A) := -| nil2 : list2 -| cons2 : A' -> list2 -> list2. + | nil2 : list2 + | cons2 : A' -> list2 -> list2. Check (list2 : Type -> Type). Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A). -#[nonuniform] Inductive bla (n:nat) := c (_ : bla (S n)). +Inductive list3 | A := nil3 | cons3 : A -> list3 (A * A)%type -> list3 A. + +Unset Uniform Inductive Parameters. + +Inductive list4 A | := nil4 | cons4 : A -> list4 -> list4. + +Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop + := Acc_in : (forall y, R y x -> Acc y) -> Acc x. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 49fb88cd8c..1d682218b6 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -125,6 +125,10 @@ CAMLPKGS ?= TIMING?= # Option for changing sorting of timing output file TIMING_SORT_BY ?= auto +# Option for changing the fuzz parameter on the output file +TIMING_FUZZ ?= 0 +# Option for changing whether to use real or user time for timing tables +TIMING_REAL?= # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -335,6 +339,19 @@ all.timing.diff: $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all .PHONY: all.timing.diff +ifeq (0,$(TIMING_REAL)) +TIMING_REAL_ARG := +TIMING_USER_ARG := --user +else +ifeq (1,$(TIMING_REAL)) +TIMING_REAL_ARG := --real +TIMING_USER_ARG := +else +TIMING_REAL_ARG := +TIMING_USER_ARG := +endif +endif + make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: @@ -342,9 +359,9 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed print-pretty-timed:: - $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_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 AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' @@ -356,7 +373,7 @@ print-pretty-single-time-diff:: $(HIDE)false else print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: @@ -695,7 +712,7 @@ $(VFILES:.v=.vok): %.vok: %.v $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing - $(SHOW)PYTHON TIMING-DIFF $< + $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" $(BEAUTYFILES): %.v.beautified: %.v diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index 3d07661d56..210901f8a7 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -4,6 +4,7 @@ from __future__ import unicode_literals from __future__ import print_function import sys import re +import argparse from io import open # This script parses the output of `make TIMED=1` into a dictionary @@ -14,18 +15,76 @@ STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?') STRIP_REP = r'\1' INFINITY = '\u221e' -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 nonnegative(arg): + v = int(arg) + if v < 0: raise argparse.ArgumentTypeError("%s is an invalid non-negative int value" % arg) + return v + +def add_sort_by(parser): + return parser.add_argument( + '--sort-by', type=str, dest='sort_by', choices=('auto', 'absolute', 'diff'), + default='auto', + help=('How to sort the table entries.\n' + + 'The "auto" method sorts by absolute time differences ' + + 'rounded towards zero to a whole-number of seconds, then ' + + 'by times in the "after" column, and finally ' + + 'lexicographically by file name. This will put the ' + + 'biggest changes in either direction first, and will ' + + 'prefer sorting by build-time over subsecond changes in ' + + 'build time (which are frequently noise); lexicographic ' + + 'sorting forces an order on files which take effectively ' + + 'no time to compile.\n' + + 'The "absolute" method sorts by the total time taken.\n' + + 'The "diff" method sorts by the signed difference in time.')) + +def add_fuzz(parser): + return parser.add_argument( + '--fuzz', dest='fuzz', metavar='N', type=nonnegative, default=0, + help=('By default, two lines are only considered the same if ' + + 'the character offsets and initial code strings match. ' + 'This option relaxes this constraint by allowing the ' + + 'character offsets to differ by up to N characters, as long ' + + 'as the total number of characters and initial code strings ' + + 'continue to match. This is useful when there are small changes ' + + 'to a file, and you want to match later lines that have not ' + + 'changed even though the character offsets have changed.')) + +def add_real(parser, single_timing=False): + return parser.add_argument( + '--real', action='store_true', + help=(r'''Use real times rather than user times. + +''' + ('''By default, the input is expected to contain lines in the format: +FILE_NAME (...user: NUMBER_IN_SECONDS...) +If --real is passed, then the lines are instead expected in the format: +FILE_NAME (...real: NUMBER_IN_SECONDS...)''' if not single_timing else +'''The input is expected to contain lines in the format: +Chars START - END COMMAND NUMBER secs (NUMBERu...)'''))) + +def add_user(parser, single_timing=False): + return parser.add_argument( + '--user', dest='real', action='store_false', + help=(r'''Use user times rather than real times. + +''' + ('''By default, the input is expected to contain lines in the format: +FILE_NAME (...real: NUMBER_IN_SECONDS...) +If --user is passed, then the lines are instead expected in the format: +FILE_NAME (...user: NUMBER_IN_SECONDS...)''' if not single_timing else +'''The input is expected to contain lines in the format: +Chars START - END COMMAND NUMBER secs (NUMBERu...)'''))) + +# N.B. We need to include default=None for nargs='*', c.f., https://bugs.python.org/issue28609#msg280180 +def add_file_name_gen(parser, prefix='', descr='file containing the build log', stddir='in', defaults=None, **kwargs): + extra = ('' if defaults is None else ' (defaults to %s if no argument is passed)' % defaults) + return parser.add_argument( + prefix + 'FILE_NAME', type=str, + help=('The name of the %s (use "-" for std%s)%s.' % (descr, stddir, extra)), + **kwargs) + +def add_file_name(parser): return add_file_name_gen(parser) +def add_after_file_name(parser): return add_file_name_gen(parser, 'AFTER_', 'file containing the "after" build log') +def add_before_file_name(parser): return add_file_name_gen(parser, 'BEFORE_', 'file containing the "before" build log') +def add_output_file_name(parser): return add_file_name_gen(parser, 'OUTPUT_', 'file to write the output table to', stddir='out', defaults='-', nargs='*', default=None) def reformat_time_string(time): @@ -45,14 +104,16 @@ def get_file_lines(file_name): lines = f.readlines() for line in lines: try: - yield line.decode('utf-8') + # Since we read the files in binary mode, we have to + # normalize Windows line endings from \r\n to \n + yield line.decode('utf-8').replace('\r\n', '\n') except UnicodeDecodeError: # invalid utf-8 pass def get_file(file_name): return ''.join(get_file_lines(file_name)) -def get_times(file_name): +def get_times(file_name, use_real=False): ''' Reads the contents of file_name, which should be the output of 'make TIMED=1', and parses it to construct a dict mapping file @@ -60,28 +121,96 @@ def get_times(file_name): using STRIP_REG and STRIP_REP. ''' lines = get_file(file_name) - reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + reg_user = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + reg_real = re.compile(r'^([^\s]+) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + reg = reg_real if use_real else reg_user times = reg.findall(lines) if all(time in ('0.00', '0.01') for name, time in times): - reg = re.compile(r'^([^\s]*) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + reg = reg_real times = reg.findall(lines) if all(STRIP_REG.search(name.strip()) for name, time in times): times = tuple((STRIP_REG.sub(STRIP_REP, name.strip()), time) for name, time in times) return dict((name, reformat_time_string(time)) for name, time in times) -def get_single_file_times(file_name): +def get_single_file_times(file_name, use_real=False): ''' Reads the contents of file_name, which should be the output of 'coqc -time', and parses it to construct a dict mapping lines to to compile durations, as strings. ''' lines = get_file(file_name) - reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', re.MULTILINE) + reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs \(([0-9\.]+)u(.*)\)$', re.MULTILINE) times = reg.findall(lines) if len(times) == 0: return dict() - longest = max(max((len(start), len(stop))) for start, stop, name, time, extra in times) + longest = max(max((len(start), len(stop))) for start, stop, name, real, user, extra in times) FORMAT = 'Chars %%0%dd - %%0%dd %%s' % (longest, longest) - return dict((FORMAT % (int(start), int(stop), name), reformat_time_string(time)) for start, stop, name, time, extra in times) + return dict((FORMAT % (int(start), int(stop), name), reformat_time_string(real if use_real else user)) for start, stop, name, real, user, extra in times) + +def fuzz_merge(l1, l2, fuzz): + '''Takes two iterables of ((start, end, code), times) and a fuzz + parameter, and yields a single iterable of ((start, stop, code), + times1, times2) + + We only give both left and right if (a) the codes are the same, + (b) the number of characters (stop - start) is the same, and (c) + the difference between left and right code locations is <= fuzz. + + We keep a current guess at the overall offset, and prefer drawing + from whichever list is earliest after correcting for current + offset. + + ''' + assert(fuzz >= 0) + cur_fuzz = 0 + l1 = list(l1) + l2 = list(l2) + cur1, cur2 = None, None + while (len(l1) > 0 or cur1 is not None) and (len(l2) > 0 or cur2 is not None): + if cur1 is None: cur1 = l1.pop(0) + if cur2 is None: cur2 = l2.pop(0) + ((s1, e1, c1), t1), ((s2, e2, c2), t2) = cur1, cur2 + assert(t1 is not None) + assert(t2 is not None) + s2_adjusted, e2_adjusted = s2 + cur_fuzz, e2 + cur_fuzz + if cur1[0] == cur2[0]: + yield (cur1, cur2) + cur1, cur2 = None, None + cur_fuzz = 0 + elif c1 == c2 and e1-s1 == e2-s2 and abs(s1 - s2) <= fuzz: + yield (((s1, e1, c1), t1), ((s2, e2, c2), t2)) + cur1, cur2 = None, None + cur_fuzz = s1 - s2 + elif s1 < s2_adjusted or (s1 == s2_adjusted and e1 <= e2): + yield (((s1, e1, c1), t1), ((s1 - cur_fuzz, e1 - cur_fuzz, c1), None)) + cur1 = None + else: + yield (((s2 + cur_fuzz, e2 + cur_fuzz, c2), None), ((s2, e2, c2), t2)) + cur2 = None + if len(l1) > 0: + for i in l1: yield (i, (i[0], None)) + elif len(l2) > 0: + for i in l2: yield ((i[0], None), i) + +def adjust_fuzz(left_dict, right_dict, fuzz): + reg = re.compile(r'Chars ([0-9]+) - ([0-9]+) (.*)$') + left_dict_list = sorted(((int(s), int(e), c), v) for ((s, e, c), v) in ((reg.match(k).groups(), v) for k, v in left_dict.items())) + right_dict_list = sorted(((int(s), int(e), c), v) for ((s, e, c), v) in ((reg.match(k).groups(), v) for k, v in right_dict.items())) + merged = list(fuzz_merge(left_dict_list, right_dict_list, fuzz)) + if len(merged) == 0: + # assert that both left and right dicts are empty + assert(not left_dict) + assert(not right_dict) + return left_dict, right_dict + longest = max(max((len(str(start1)), len(str(stop1)), len(str(start2)), len(str(stop2)))) for ((start1, stop1, code1), t1), ((start2, stop2, code2), t2) in merged) + FORMAT1 = 'Chars %%0%dd - %%0%dd %%s' % (longest, longest) + FORMAT2 = 'Chars %%0%dd-%%0%dd ~ %%0%dd-%%0%dd %%s' % (longest, longest, longest, longest) + if fuzz == 0: + left_dict = dict((FORMAT1 % k, t1) for (k, t1), _ in merged if t1 is not None) + right_dict = dict((FORMAT1 % k, t2) for _, (k, t2) in merged if t2 is not None) + else: + left_dict = dict((FORMAT2 % (s1, e1, s2, e2, c1), t1) for ((s1, e1, c1), t1), ((s2, e2, c2), t2) in merged if t1 is not None) + right_dict = dict((FORMAT2 % (s1, e1, s2, e2, c1), t2) for ((s1, e1, c1), t1), ((s2, e2, c2), t2) in merged if t2 is not None) + return left_dict, right_dict def fix_sign_for_sorting(num, descending=True): return -num if descending else num diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index fddf75f39f..a28da43043 100755 --- a/tools/make-both-single-timing-files.py +++ b/tools/make-both-single-timing-files.py @@ -1,12 +1,17 @@ #!/usr/bin/env python3 -import sys from TimeFileMaker import * if __name__ == '__main__': - 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''' - 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:]) + parser = argparse.ArgumentParser(description=r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table''') + add_sort_by(parser) + add_user(parser, single_timing=True) + add_fuzz(parser) + add_after_file_name(parser) + add_before_file_name(parser) + add_output_file_name(parser) + args = parser.parse_args() + left_dict = get_single_file_times(args.AFTER_FILE_NAME, use_real=args.real) + right_dict = get_single_file_times(args.BEFORE_FILE_NAME, use_real=args.real) + left_dict, right_dict = adjust_fuzz(left_dict, right_dict, fuzz=args.fuzz) + table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=args.sort_by) + print_or_write_table(table, args.OUTPUT_FILE_NAME) diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py index 8937d63c2f..5d88548bba 100755 --- a/tools/make-both-time-files.py +++ b/tools/make-both-time-files.py @@ -1,16 +1,15 @@ #!/usr/bin/env python3 -import sys from TimeFileMaker import * if __name__ == '__main__': - 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...) -''' - 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:]) + parser = argparse.ArgumentParser(description=r'''Formats timing information from the output of two invocations of `make TIMED=1` into a sorted table.''') + add_sort_by(parser) + add_real(parser) + add_after_file_name(parser) + add_before_file_name(parser) + add_output_file_name(parser) + args = parser.parse_args() + left_dict = get_times(args.AFTER_FILE_NAME, use_real=args.real) + right_dict = get_times(args.BEFORE_FILE_NAME, use_real=args.real) + table = make_diff_table_string(left_dict, right_dict, sort_by=args.sort_by) + print_or_write_table(table, args.OUTPUT_FILE_NAME) diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py index ad0a04ab07..3df7d7e584 100755 --- a/tools/make-one-time-file.py +++ b/tools/make-one-time-file.py @@ -3,19 +3,11 @@ import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] - HELP_STRING = r'''Formats timing information from the output 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) < 2 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: - times_dict = get_times(sys.argv[1]) - table = make_table_string(times_dict) - print_or_write_table(table, sys.argv[2:]) + parser = argparse.ArgumentParser(description=r'''Formats timing information from the output of `make TIMED=1` into a sorted table.''') + add_real(parser) + add_file_name(parser) + add_output_file_name(parser) + args = parser.parse_args() + times_dict = get_times(args.FILE_NAME, use_real=args.real) + table = make_table_string(times_dict) + print_or_write_table(table, args.OUTPUT_FILE_NAME) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index d711c9aea0..85f2bf3708 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -456,9 +456,19 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in let arities, relevances, arityconcl, indimpls = List.split4 arities in - let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in + let lift1_ctx ctx = + let t = EConstr.it_mkProd_or_LetIn EConstr.mkProp ctx in + let t = EConstr.Vars.lift 1 t in + let ctx, _ = EConstr.decompose_prod_assum sigma t in + ctx + in + let ctx_params_lifted, fullarities = CList.fold_left_map + (fun ctx_params c -> lift1_ctx ctx_params, EConstr.it_mkProd_or_LetIn c ctx_params) + ctx_params + arities + in let env_ar = push_types env_uparams indnames relevances fullarities in - let env_ar_params = EConstr.push_rel_context ctx_params env_ar in + let env_ar_params = EConstr.push_rel_context ctx_params_lifted env_ar in (* Compute interpretation metadatas *) let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in @@ -509,6 +519,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 +let eq_params (up1,p1) (up2,p2) = + eq_local_binders up1 up2 && Option.equal eq_local_binders p1 p2 + let extract_coercions indl = let mkqid (_,({CAst.v=id},_)) = qualid_of_ident id in let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in @@ -519,7 +532,7 @@ let extract_params indl = match paramsl with | [] -> anomaly (Pp.str "empty list of inductive types.") | params::paramsl -> - if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str + if not (List.for_all (eq_params params) paramsl) then user_err Pp.(str "Parameters should be syntactically the same for each inductive type."); params @@ -544,7 +557,12 @@ type uniform_inductive_flag = let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite = let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in + let indl = match params with + | uparams, Some params -> (uparams, params, indl) + | params, None -> match uniform with + | UniformParameters -> (params, [], indl) + | NonUniformParameters -> ([], params, indl) + in let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in (* Declare the mutual inductive block with its associated schemes *) ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls); diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 5e98f5ddc0..3181bcc4bc 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -249,7 +249,6 @@ type (_, _) entry = | TTName : ('self, lname) entry | TTReference : ('self, qualid) entry | TTBigint : ('self, string) entry -| TTString : ('self, string) entry | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry | TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry @@ -370,14 +369,12 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = | TTName -> MayRecNo (Aentry Prim.name) | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders) | TTBigint -> MayRecNo (Aentry Prim.bigint) -| TTString -> MayRecNo (Aentry Prim.string) | TTReference -> MayRecNo (Aentry Constr.global) let interp_entry forpat e = match e with | ETProdName -> TTAny TTName | ETProdReference -> TTAny TTReference | ETProdBigint -> TTAny TTBigint -| ETProdString -> TTAny TTString | ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat)) | ETProdPattern p -> TTAny (TTPattern p) | ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat)) @@ -417,11 +414,6 @@ match e with | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v))) | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v))) end -| TTString -> - begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (String v)) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (String v)) - end | TTReference -> begin match forpat with | ForConstr -> push_constr subst (CAst.make @@ CRef (v, None)) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 97c9d23c68..d597707d12 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -395,9 +395,10 @@ GRAMMAR EXTEND Gram ; inductive_definition: [ [ oc = opt_coercion; id = ident_decl; indpar = binders; + extrapar = OPT [ "|"; p = binders -> { p } ]; c = OPT [ ":"; c = lconstr -> { c } ]; lc=opt_constructors_or_fields; ntn = decl_notation -> - { (((oc,id),indpar,c,lc),ntn) } ] ] + { (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ] ; constructor_list_or_record_decl: [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l } @@ -1234,7 +1235,6 @@ GRAMMAR EXTEND Gram syntax_extension_type: [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal } | IDENT "bigint" -> { ETBigint } - | IDENT "string" -> { ETString } | IDENT "binder" -> { ETBinder true } | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) } | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) } diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index d39ee60c25..7794b0a37a 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -396,7 +396,7 @@ let unparsing_metavar i from typs = let x = List.nth typs (i-1) in let prec = unparsing_precedence_of_entry_type from x in match x with - | ETConstr _ | ETGlobal | ETBigint | ETString -> + | ETConstr _ | ETGlobal | ETBigint -> UnpMetaVar (i,prec) | ETPattern _ -> UnpBinderMetaVar (i,prec) @@ -686,7 +686,6 @@ let prod_entry_type = function | ETIdent -> ETProdName | ETGlobal -> ETProdReference | ETBigint -> ETProdBigint - | ETString -> ETProdString | ETBinder _ -> assert false (* See check_binder_type *) | ETConstr (s,_,p) -> ETProdConstr (s,p) | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n) @@ -990,7 +989,7 @@ let set_entry_type from n etyps (x,typ) = | ETConstr (s,bko,n), InternalProd -> ETConstr (s,bko,(n,InternalProd)) | ETPattern (b,n), _ -> ETPattern (b,n) - | (ETIdent | ETBigint | ETString | ETGlobal | ETBinder _ as x), _ -> x + | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x with Not_found -> ETConstr (from,None,(make_lev n from,typ)) in (x,typ) @@ -1012,7 +1011,7 @@ let join_auxiliary_recursive_types recvars etyps = let internalization_type_of_entry_type = function | ETBinder _ -> NtnInternTypeOnlyBinder - | ETConstr _ | ETBigint | ETString | ETGlobal + | ETConstr _ | ETBigint | ETGlobal | ETIdent | ETPattern _ -> NtnInternTypeAny let set_internalization_type typs = @@ -1034,7 +1033,7 @@ let make_interpretation_type isrec isonlybinding = function (* Others *) | ETIdent -> NtnTypeBinder NtnParsedAsIdent | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *) - | ETBigint | ETString | ETGlobal -> NtnTypeConstr + | ETBigint | ETGlobal -> NtnTypeConstr | ETBinder _ -> if isrec then NtnTypeBinderList else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.") @@ -1098,8 +1097,6 @@ type entry_coercion_kind = | IsEntryCoercion of notation_entry_level | IsEntryGlobal of string * int | IsEntryIdent of string * int - | IsEntryNumeral of string * int - | IsEntryString of string * int let is_coercion = function | Some (custom,n,_,[e]) -> @@ -1111,8 +1108,6 @@ let is_coercion = function else Some (IsEntryCoercion subentry) | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n)) | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n)) - | ETBigint, InCustomEntry s -> Some (IsEntryNumeral (s,n)) - | ETString, InCustomEntry s -> Some (IsEntryString (s,n)) | _ -> None) | Some _ -> assert false | None -> None @@ -1154,7 +1149,7 @@ let find_precedence custom lev etyps symbols onlyprint = user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in (try match List.assoc x etyps, custom with | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test () - | (ETIdent | ETBigint | ETString | ETGlobal), _ -> + | (ETIdent | ETBigint | ETGlobal), _ -> begin match lev with | None -> ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0) @@ -1380,8 +1375,6 @@ let open_notation i (_, nobj) = | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n - | Some (IsEntryNumeral (entry,n)) -> Notation.declare_custom_entry_has_numeral entry n - | Some (IsEntryString (entry,n)) -> Notation.declare_custom_entry_has_string entry n | None -> ()) end diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 0cf407619b..314c423f65 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -126,7 +126,6 @@ open Pputils | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n) | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko | ETBigint -> str "bigint" - | ETString -> str "string" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" @@ -811,11 +810,12 @@ let string_of_definition_object_kind = let open Decls in function | RecordDecl (c,fs) -> pr_record_decl c fs in - let pr_oneind key (((coe,iddecl),indpar,s,lc),ntn) = + let pr_oneind key (((coe,iddecl),(indupar,indpar),s,lc),ntn) = hov 0 ( str key ++ spc() ++ (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++ - pr_and_type_binders_arg indpar ++ + pr_and_type_binders_arg indupar ++ + pr_opt (fun p -> str "|" ++ spc() ++ pr_and_type_binders_arg p) indpar ++ pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++ str" :=") ++ pr_constructor_list lc ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e469323f50..63fc587f71 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -623,18 +623,16 @@ let should_treat_as_cumulative cum poly = else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") | None -> poly && is_polymorphic_inductive_cumulativity () -let uniform_att = - let get_uniform_inductive_parameters = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Uniform"; "Inductive"; "Parameters"] - ~value:false - in - let open Attributes.Notations in - Attributes.bool_attribute ~name:"uniform" ~on:"uniform" ~off:"nonuniform" >>= fun u -> - let u = match u with Some u -> u | None -> get_uniform_inductive_parameters () in - let u = if u then ComInductive.UniformParameters else ComInductive.NonUniformParameters in - return u +let get_uniform_inductive_parameters = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Uniform"; "Inductive"; "Parameters"] + ~value:false + +let should_treat_as_uniform () = + if get_uniform_inductive_parameters () + then ComInductive.UniformParameters + else ComInductive.NonUniformParameters let vernac_record ~template udecl cum k poly finite records = let cumulative = should_treat_as_cumulative cum poly in @@ -682,6 +680,7 @@ let finite_of_kind = let open Declarations in function indicates whether the type is inductive, co-inductive or neither. *) let vernac_inductive ~atts cum lo kind indl = + let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in let open Pp in let udecl, indl = extract_inductive_udecl indl in if Dumpglob.dump () then @@ -710,12 +709,14 @@ let vernac_inductive ~atts cum lo kind indl = if Option.has_some is_defclass then (* Definitional class case *) let (id, bl, c, l) = Option.get is_defclass in + let bl = match bl with + | bl, None -> bl + | _ -> CErrors.user_err Pp.(str "Definitional classes do not support the \"|\" syntax.") + in let (coe, (lid, ce)) = l in let coe' = if coe then Some true else None in let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce), - { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } - in - let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in + { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (* Mutual record case *) @@ -732,12 +733,15 @@ let vernac_inductive ~atts cum lo kind indl = let () = List.iter check_where indl in let unpack ((id, bl, c, decl), _) = match decl with | RecordDecl (oc, fs) -> + let bl = match bl with + | bl, None -> bl + | _ -> CErrors.user_err Pp.(str "Records do not support the \"|\" syntax.") + in (id, bl, c, oc, fs) | Constructors _ -> assert false (* ruled out above *) in let kind = match kind with Class _ -> Class false | _ -> kind in let recordl = List.map unpack indl in - let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in vernac_record ~template udecl cum kind poly finite recordl else if List.for_all is_constructor indl then (* Mutual inductive case *) @@ -761,12 +765,9 @@ let vernac_inductive ~atts cum lo kind indl = | RecordDecl _ -> assert false (* ruled out above *) in let indl = List.map unpack indl in - let (template, poly), uniform = - Attributes.(parse Notations.(template ++ polymorphic ++ uniform_att) atts) - in let cumulative = should_treat_as_cumulative cum poly in - ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly - ~private_ind:lo ~uniform finite + let uniform = should_treat_as_uniform () in + ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 3610240634..45018a246c 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -163,12 +163,15 @@ type constructor_expr = (lident * constr_expr) with_coercion type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * (local_decl_expr * record_field_attr) list +type inductive_params_expr = local_binder_expr list * local_binder_expr list option +(** If the option is nonempty the "|" marker was used *) + type inductive_expr = - ident_decl with_coercion * local_binder_expr list * constr_expr option * + ident_decl with_coercion * inductive_params_expr * constr_expr option * constructor_list_or_record_decl_expr type one_inductive_expr = - lident * local_binder_expr list * constr_expr option * constructor_expr list + lident * inductive_params_expr * constr_expr option * constructor_expr list type typeclass_constraint = name_decl * Glob_term.binding_kind * constr_expr and typeclass_context = typeclass_constraint list |