diff options
42 files changed, 133 insertions, 74 deletions
diff --git a/.github/SUPPORT.md b/.github/SUPPORT.md index b6f2e942e9..978f011f23 100644 --- a/.github/SUPPORT.md +++ b/.github/SUPPORT.md @@ -1,28 +1,22 @@ -# Support # +[![Zulip][zulip-badge]][zulip-link] +[![Discourse][discourse-badge]][discourse-link] + +[discourse-badge]: https://img.shields.io/badge/Discourse-forum-informational.svg +[discourse-link]: https://coq.discourse.group/ -Get in touch with the user community and ask questions about Coq on -our [Discourse forum][]. Posts in other languages than English are -explicitly welcome there. There is also a historic mailing list called -the [Coq-Club][] which has lots of subscribers, and an IRC channel -(`irc://irc.freenode.net/#coq`). +[zulip-badge]: https://img.shields.io/badge/Zulip-chat-informational.svg +[zulip-link]: https://coq.zulipchat.com/ + +# Support # -In addition, you may also ask questions about Coq on [Stack -Overflow][] (use the tag [coq][Stack Overflow tag]) or on the -meta-theory of Coq on the [TCS Stack Exchange][] (which also has a -[coq][TCS SE tag] tag). +<!-- content copied verbatim from "Questions and discussion" in README.md --> -You can reach the Coq development team through the [development -category][] of the above mentioned Discourse forum, the [Gitter -channel][], and of course the bug tracker. +We have a number of channels to reach the user community and the +development team: -See also [coq.inria.fr/community](https://coq.inria.fr/community.html). +- Our [Zulip chat][zulip-link], for casual and high traffic discussions. +- Our [Discourse forum][discourse-link], for more structured and easily browsable discussions and Q&A. +- Our historical mailing list, the [Coq-Club](https://sympa.inria.fr/sympa/info/coq-club). -[Discourse forum]: https://coq.discourse.group -[Coq-Club]: https://sympa.inria.fr/sympa/arc/coq-club -[Stack Overflow]: https://stackoverflow.com -[Stack Overflow tag]: https://stackoverflow.com/questions/tagged/coq -[TCS Stack Exchange]: https://cstheory.stackexchange.com/ -[TCS SE tag]: https://cstheory.stackexchange.com/questions/tagged/coq -[development category]: https://coq.discourse.group/c/coq-development -[Gitter channel]: https://gitter.im/coq/coq -[bug tracker]: https://github.com/coq/coq/issues +See also [coq.inria.fr/community](https://coq.inria.fr/community.html), which +lists several other active platforms. diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 4139a0dbe5..87101ecae7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-05-18-V3" + CACHEKEY: "bionic_coq-V2020-05-19-V33" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -698,6 +698,9 @@ library:ci-coquelicot: library:ci-cross_crypto: extends: .ci-template +library:ci-engine_bench: + extends: .ci-template + library:ci-fcsl_pcm: extends: .ci-template diff --git a/.ocamlformat b/.ocamlformat index 62e609fb55..a0d4ef6bbb 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,4 +1,4 @@ -version=0.14.0 +version=0.14.2 profile=ocamlformat # to enable a whole directory, put "disable=false" in dir/.ocamlformat @@ -11,4 +11,4 @@ cases-exp-indent=2 field-space=loose exp-grouping=preserve break-cases=fit -doc-comments-val=before +doc-comments=before diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md index 0720cf6210..0d8751de7e 100644 --- a/CODE_OF_CONDUCT.md +++ b/CODE_OF_CONDUCT.md @@ -11,7 +11,7 @@ Their goal is that everyone feels safe and welcome when contributing to Coq or interacting with others in Coq related forums. These rules apply to all spaces managed by the Coq development team. -This includes the GitHub repository, the mailing lists, the Gitter channel, +This includes the GitHub repository, the Discourse forum, the Zulip chat, the mailing lists, physical events like Coq working groups and workshops, and any other forums created or managed by the development team which the community uses for communication. In addition, violations of these rules outside these spaces may diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 525ced7fee..8a09e43c94 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -179,7 +179,8 @@ Learn how to write a Coq plugin, and about best practices, in the Coq progress, so do not hesitate to expand it, or ask questions. If you want quick feedback on best practices, or how to talk to the -Coq API, a good place to hang out is the Coq [Gitter channel][Gitter]. +Coq API, a good place to hang out is the [Coq devs & plugin devs +stream][Zulip-dev] of our Zulip chat. Finally, we strongly encourage authors of plugins to submit their plugins to join Coq's continuous integration (CI) early on. Indeed, @@ -285,7 +286,7 @@ GitHub account). You can file a bug for any of the following: It would help if you search the existing issues before reporting a bug. This can be difficult, so consider it extra credit. We don't mind duplicate bug reports. If unsure, you are always very welcome to -ask on our [Discourse forum][Discourse] or [Gitter chat][Gitter] +ask on our [Discourse forum][Discourse] or [Zulip chat][Zulip] before, after, or while writing a bug report. It is better if you can test that your bug is still present in the @@ -364,7 +365,7 @@ Being in this team will grant you the following access: idea for a new feature). - **Creating new labels:** if you feel a `part:` label is missing, do not hesitate to create it. If you are not sure, you may discuss it - with other contributors and developers on [Gitter][] first. + with other contributors and developers on [Zulip][Zulip-dev] first. - **Closing issues:** if a bug cannot be reproduced anymore, is a duplicate, or should not be considered a bug report in the first place, you should close it. When doing so, try putting an @@ -1133,7 +1134,7 @@ before a change is ready on your side. When opening a draft PR, make sure to give it a descriptive enough title so that interested developers still notice it in their notification feed. You may also advertise it by talking about it in -our [developer chat][Gitter]. If you know which developer would be +our [developer chat][Zulip-dev]. If you know which developer would be able to provide useful feedback to you, you may also ping them. ###### Turning a PR into draft mode ###### @@ -1182,8 +1183,9 @@ documentation is still a work-in-progress. ### Online forum and chat to talk to developers ### We have a [Discourse forum][Discourse] (see in particular the [Coq -development category][Discourse-development-category]) and a [Gitter -chat][Gitter]. Feel free to join any of them and ask questions. +development][Discourse-development-category] category) and a [Zulip +chat][Zulip] (see in particular the [Coq devs & plugin devs][Zulip-dev] +stream). Feel free to join any of them and ask questions. People are generally happy to help and very reactive. Obviously, the issue tracker is also a good place to ask questions, @@ -1267,7 +1269,6 @@ can be found [on the wiki][wiki-CUDW]. [GitHub-wiki-extensions]: https://help.github.com/en/articles/editing-wiki-content [GitLab-coq]: https://gitlab.com/coq [GitLab-doc]: https://docs.gitlab.com/ -[Gitter]: https://gitter.im/coq/coq [JasonGross-coq-tools]: https://github.com/JasonGross/coq-tools [jenkins-doc]: https://github.com/coq/coq/wiki/Jenkins-(automated-benchmarking) [kind-documentation]: https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+label%3A%22kind%3A+documentation%22 @@ -1311,3 +1312,5 @@ can be found [on the wiki][wiki-CUDW]. [wiki-CUDW]: https://github.com/coq/coq/wiki/CoqImplementorsWorkshop [wiki-WG]: https://github.com/coq/coq/wiki/Coq-Working-Groups [YouTube]: https://www.youtube.com/channel/UCbJo6gYYr0OF18x01M4THdQ +[Zulip]: https://coq.zulipchat.com +[Zulip-dev]: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs diff --git a/Makefile.ci b/Makefile.ci index af92d476ba..9b7008f765 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -23,6 +23,7 @@ CI_TARGETS= \ ci-coq_tools \ ci-coqprime \ ci-elpi \ + ci-engine_bench \ ci-ext_lib \ ci-equations \ ci-fcsl_pcm \ @@ -2,7 +2,8 @@ [![GitLab][gitlab-badge]][gitlab-link] [![Azure Pipelines][azure-badge]][azure-link] -[![Gitter][gitter-badge]][gitter-link] +[![Zulip][zulip-badge]][zulip-link] +[![Discourse][discourse-badge]][discourse-link] [![DOI][doi-badge]][doi-link] [gitlab-badge]: https://gitlab.com/coq/coq/badges/master/pipeline.svg @@ -11,8 +12,11 @@ [azure-badge]: https://dev.azure.com/coq/coq/_apis/build/status/coq.coq?branchName=master [azure-link]: https://dev.azure.com/coq/coq/_build/latest?definitionId=1?branchName=master -[gitter-badge]: https://badges.gitter.im/coq/coq.svg -[gitter-link]: https://gitter.im/coq/coq +[discourse-badge]: https://img.shields.io/badge/Discourse-forum-informational.svg +[discourse-link]: https://coq.discourse.group/ + +[zulip-badge]: https://img.shields.io/badge/Zulip-chat-informational.svg +[zulip-link]: https://coq.zulipchat.com/ [doi-badge]: https://zenodo.org/badge/DOI/10.5281/zenodo.1003420.svg [doi-link]: https://doi.org/10.5281/zenodo.1003420 @@ -102,12 +106,12 @@ approach some problems you may encounter. We have a number of channels to reach the user community and the development team: -- Our [Discourse forum](https://coq.discourse.group). -- Our mailing list, the [Coq-Club](https://sympa.inria.fr/sympa/info/coq-club). -- Our [Gitter channel][gitter-link], which is a good way to reach - developers for quick chat and development questions. +- Our [Zulip chat][zulip-link], for casual and high traffic discussions. +- Our [Discourse forum][discourse-link], for more structured and easily browsable discussions and Q&A. +- Our historical mailing list, the [Coq-Club](https://sympa.inria.fr/sympa/info/coq-club). -See also [coq.inria.fr/community](https://coq.inria.fr/community.html). +See also [coq.inria.fr/community](https://coq.inria.fr/community.html), which +lists several other active platforms. ## Bug reports diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 5f7d0b5789..19ba9de245 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -239,6 +239,13 @@ : "${elpi_hb_CI_ARCHIVEURL:=${elpi_hb_CI_GITURL}/archive}" ######################################################################## +# Engine-Bench +######################################################################## +: "${engine_bench_CI_REF:=master}" +: "${engine_bench_CI_GITURL:=https://github.com/mit-plv/engine-bench}" +: "${engine_bench_CI_ARCHIVEURL:=${engine_bench_CI_GITURL}/archive}" + +######################################################################## # fcsl-pcm ######################################################################## : "${fcsl_pcm_CI_REF:=master}" diff --git a/dev/ci/ci-engine_bench.sh b/dev/ci/ci-engine_bench.sh new file mode 100755 index 0000000000..fda7649f88 --- /dev/null +++ b/dev/ci/ci-engine_bench.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download engine_bench + +( cd "${CI_BUILD_DIR}/engine_bench" && make coq && make coq-perf-Sanity ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 51a602303a..0d2f1dfbc7 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-05-18-V3" +# CACHEKEY: "bionic_coq-V2020-05-19-V33" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -58,7 +58,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ # EDGE switch ENV COMPILER_EDGE="4.10.0" \ - BASE_OPAM_EDGE="dune.2.5.0 dune-release.1.3.3 ocamlformat.0.14.0" + BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.14.2" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index fb84155392..bfb25e72dd 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/807ca93fadd5197c2260490de0c76e500562dc05.tar.gz"; - sha256 = "10yq8bnls77fh3pk5chkkb1sv5lbdgyk1rr2v9xn71rr1k2x563p"; + url = "https://github.com/NixOS/nixpkgs/archive/17812e653d89c46d68b7b10e290b1c16758f4e47.tar.gz"; + sha256 = "1zcb70dyfqc8l2ywpbvxmpfshapdi0g365m3rhmwpagqg47pnyxs"; }) diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index ce64aebdc7..82e4bd1e1e 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -49,10 +49,26 @@ ask_confirmation() { fi } +curl_paginate_array() { + # as per https://developer.github.com/v3/guides/traversing-with-pagination/#changing-the-number-of-items-received, GitHub will never give us more than 100 + url="$1?per_page=100" + # we keep fetching pages until the response is below the per-page limit (possibly 0 elements) + page=1 + while true; do + response="$(curl -s "${url}&page=${page}")" + echo "${response}" + if [ "$(jq 'length' <<< "$response")" -lt 100 ]; then # done + break + fi + page=$(($page + 1)) + done | jq '[.[]]' # we concatenate the arrays +} + check_util jq check_util curl check_util git check_util gpg +check_util grep # command line parsing @@ -70,6 +86,8 @@ fi # Fetching PR metadata +# The main API call returns a dict/object, not an array, so we don't +# bother paginating PRDATA=$(curl -s "$API/pulls/$PR") TITLE=$(echo "$PRDATA" | jq -r '.title') @@ -203,7 +221,7 @@ fi # Generate commit message info "Fetching review data" -reviews=$(curl -s "$API/pulls/$PR/reviews") +reviews=$(curl_paginate_array "$API/pulls/$PR/reviews") msg="Merge PR #$PR: $TITLE" has_state() { diff --git a/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst b/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst new file mode 100644 index 0000000000..5b35090d7e --- /dev/null +++ b/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst @@ -0,0 +1,5 @@ +- **Changed:** + :cmd:Redirect now obeys the :opt:`Printing Width` and + :opt:`Printing Depth` flags. + (`#12358 <https://github.com/coq/coq/pull/12358>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst b/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst new file mode 100644 index 0000000000..8a43f5af94 --- /dev/null +++ b/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst @@ -0,0 +1,4 @@ +- **Changed:** + The pretty-timed scripts and targets now print a newline at the end of their + tables, rather than creating text with no trailing newline (`#12368 + <https://github.com/coq/coq/pull/12368>`_, by Jason Gross). diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired index 541b307b5e..85aeab2c69 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired @@ -3,4 +3,4 @@ 0m00.47s | 394716 ko | Total Time / Peak Mem | 0m00.45s | 394392 ko || +0m00.01s || 324 ko | +4.44% | +0.08% ----------------------------------------------------------------------------------------------------------------------------- 0m00.42s | 394716 ko | Fast.vo | 0m00.02s | 57164 ko || +0m00.40s || 337552 ko | +1999.99% | +590.49% -0m00.05s | 57124 ko | Slow.vo | 0m00.43s | 394392 ko || -0m00.38s || -337268 ko | -88.37% | -85.51%
\ No newline at end of file +0m00.05s | 57124 ko | Slow.vo | 0m00.43s | 394392 ko || -0m00.38s || -337268 ko | -88.37% | -85.51% diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired index 71e4ee0b32..ed5454b480 100644 --- a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired +++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired @@ -1,9 +1,9 @@ After | Code | Before || Change | % Change ---------------------------------------------------------------------------------------------------- - 0m14.06s | Total | 0m00.72s || +0m13.34s | +1854.02% + 0m15.00s | Total | 0m00.72s || +0m14.28s | +1983.61% ---------------------------------------------------------------------------------------------------- -0m13.582s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.353s || +0m13.22s | +3747.59% -0m00.335s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.225s || +0m00.11s | +48.88% -0m00.152s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.142s || +0m00.01s | +7.04% +0m14.578s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.356s || +0m14.22s | +3994.94% +0m00.284s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.225s || +0m00.05s | +26.22% + 0m00.14s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.139s || +0m00.00s | +0.71% 0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | N/A || +0m00.00s | N/A - N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | 0m00.s || +0m00.00s | N/A diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-absolute.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-absolute.log.expected index e7d289858b..948e28fbc6 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-absolute.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-absolute.log.expected @@ -23,4 +23,4 @@ 0m07.33s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s | 578344 ko || -0m00.07s || -3956 ko | -0.94% | -0.68% 0m01.93s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s | 546112 ko || +0m00.19s || -1940 ko | +11.56% | -0.35% 0m01.85s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.95s | 648632 ko || -0m00.09s || -2332 ko | -5.12% | -0.35% - 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12%
\ No newline at end of file + 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-auto.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-auto.log.expected index 36f86e0e1e..ea36822c8d 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-auto.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-auto.log.expected @@ -23,4 +23,4 @@ 0m07.33s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s | 578344 ko || -0m00.07s || -3956 ko | -0.94% | -0.68% 0m01.93s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s | 546112 ko || +0m00.19s || -1940 ko | +11.56% | -0.35% 0m01.85s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.95s | 648632 ko || -0m00.09s || -2332 ko | -5.12% | -0.35% - 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12%
\ No newline at end of file + 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-diff.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-diff.log.expected index 6415223693..b6c21a3145 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-diff.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-diff.log.expected @@ -23,4 +23,4 @@ 3m22.96s | 3302508 ko | Specific/NISTP256/AMD64/femul | 3m37.80s | 3307052 ko || -0m14.84s || -4544 ko | -6.81% | -0.13% 2m35.79s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m59.21s | 1549104 ko || -0m23.42s || -94408 ko | -13.06% | -6.09% 3m01.77s | 1589516 ko | Specific/solinas32_2e255m765_13limbs/femul | 3m27.94s | 1656912 ko || -0m26.16s || -67396 ko | -12.58% | -4.06% - 4m16.77s | 1617000 ko | Specific/X25519/C64/ladderstep | 5m16.83s | 1621500 ko || -1m00.06s || -4500 ko | -18.95% | -0.27%
\ No newline at end of file + 4m16.77s | 1617000 ko | Specific/X25519/C64/ladderstep | 5m16.83s | 1621500 ko || -1m00.06s || -4500 ko | -18.95% | -0.27% 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 index 36f86e0e1e..ea36822c8d 100644 --- 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 @@ -23,4 +23,4 @@ 0m07.33s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s | 578344 ko || -0m00.07s || -3956 ko | -0.94% | -0.68% 0m01.93s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s | 546112 ko || +0m00.19s || -1940 ko | +11.56% | -0.35% 0m01.85s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.95s | 648632 ko || -0m00.09s || -2332 ko | -5.12% | -0.35% - 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12%
\ No newline at end of file + 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-absolute.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-absolute.log.expected index 84d20f484a..a964c29da8 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-absolute.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-absolute.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.22s | 578344 ko || -0m00.04s || -3956 ko | -0.55% | -0.68% 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.58s | 546112 ko || +0m00.13s || -1940 ko | +8.86% | -0.35% 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.72s | 648632 ko || -0m00.05s || -2332 ko | -2.90% | -0.35% - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12%
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-auto.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-auto.log.expected index 7576dca88b..59af8c3145 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-auto.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-auto.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.22s | 578344 ko || -0m00.04s || -3956 ko | -0.55% | -0.68% 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.58s | 546112 ko || +0m00.13s || -1940 ko | +8.86% | -0.35% 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.72s | 648632 ko || -0m00.05s || -2332 ko | -2.90% | -0.35% - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12%
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-diff.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-diff.log.expected index 1173a6fe29..5ee974c9f3 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-diff.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-diff.log.expected @@ -23,4 +23,4 @@ 3m09.62s | 3302508 ko | Specific/NISTP256/AMD64/femul | 3m22.52s | 3307052 ko || -0m12.90s || -4544 ko | -6.36% | -0.13% 2m23.70s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m44.11s | 1549104 ko || -0m20.41s || -94408 ko | -12.43% | -6.09% 2m48.52s | 1589516 ko | Specific/solinas32_2e255m765_13limbs/femul | 3m12.95s | 1656912 ko || -0m24.42s || -67396 ko | -12.66% | -4.06% - 4m01.34s | 1617000 ko | Specific/X25519/C64/ladderstep | 4m59.49s | 1621500 ko || -0m58.15s || -4500 ko | -19.41% | -0.27%
\ No newline at end of file + 4m01.34s | 1617000 ko | Specific/X25519/C64/ladderstep | 4m59.49s | 1621500 ko || -0m58.15s || -4500 ko | -19.41% | -0.27% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected index 7576dca88b..59af8c3145 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.22s | 578344 ko || -0m00.04s || -3956 ko | -0.55% | -0.68% 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.58s | 546112 ko || +0m00.13s || -1940 ko | +8.86% | -0.35% 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.72s | 648632 ko || -0m00.05s || -2332 ko | -2.90% | -0.35% - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12%
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected index 94122d8190..317497c68a 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline 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 index 94122d8190..317497c68a 100644 --- 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 @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected index 6104c78380..ee9fca7eb4 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected @@ -304,4 +304,4 @@ 0m00.04s | 54440 ko | bedrock2/deps/coqutil/src/dlet 0m00.04s | 54804 ko | bedrock2/deps/coqutil/src/sanity 0m00.04s | 56096 ko | bedrock2/deps/riscv-coq/src/Utility/MMIOTrace - 0m00.03s | 54716 ko | bedrock2/compiler/src/util/LogGoal
\ No newline at end of file + 0m00.03s | 54716 ko | bedrock2/compiler/src/util/LogGoal 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 index 76b0a35cb2..37f144b19b 100644 --- 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 @@ -26,4 +26,4 @@ 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 + 0m00.s | Chars 200-257 ~ 220-277 [Goal~_~List.repeat~Z.div_eucl~...] | 0m00.s || +0m00.00s | N/A 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 index 1e27d5d12b..a77215b67d 100644 --- 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 @@ -26,4 +26,4 @@ 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 + 0m00.s | Chars 195-199 ~ 215-219 [Qed.] | 0m00.s || +0m00.00s | N/A diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-absolute.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-absolute.log.expected index 2a2d2c1b2f..9d6231f2ce 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-absolute.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-absolute.log.expected @@ -23,4 +23,4 @@ 0m01.85s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.95s | 648632 ko || -0m00.09s || -2332 ko | -5.12% | -0.35% 0m07.33s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s | 578344 ko || -0m00.07s || -3956 ko | -0.94% | -0.68% 0m01.93s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s | 546112 ko || +0m00.19s || -1940 ko | +11.56% | -0.35% - 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12%
\ No newline at end of file + 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-auto.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-auto.log.expected index 7e4cfaec1c..4864c1aaf7 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-auto.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-auto.log.expected @@ -23,4 +23,4 @@ 0m27.81s | 756080 ko | Specific/NISTP256/AMD64/fenz | 0m28.91s | 756216 ko || -0m01.10s || -136 ko | -3.80% | -0.01% 0m22.81s | 766300 ko | Specific/X25519/C64/feadd | 0m23.43s | 766168 ko || -0m00.62s || 132 ko | -2.64% | +0.01% 0m11.15s | 687760 ko | Specific/X25519/C64/Synthesis | 0m11.23s | 687812 ko || -0m00.08s || -52 ko | -0.71% | -0.00% - 0m31.00s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m32.08s | 765212 ko || -0m01.07s || -4 ko | -3.36% | -0.00%
\ No newline at end of file + 0m31.00s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m32.08s | 765212 ko || -0m01.07s || -4 ko | -3.36% | -0.00% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-diff.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-diff.log.expected index 7842f91f1f..27d3a9c683 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-diff.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-diff.log.expected @@ -23,4 +23,4 @@ 0m43.34s | 793376 ko | Specific/NISTP256/AMD64/fesub | 0m43.78s | 799668 ko || -0m00.43s || -6292 ko | -1.00% | -0.78% 0m39.72s | 825448 ko | Specific/X25519/C64/femul | 0m42.98s | 839624 ko || -0m03.25s || -14176 ko | -7.58% | -1.68% 3m01.77s | 1589516 ko | Specific/solinas32_2e255m765_13limbs/femul | 3m27.94s | 1656912 ko || -0m26.16s || -67396 ko | -12.58% | -4.06% - 2m35.79s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m59.21s | 1549104 ko || -0m23.42s || -94408 ko | -13.06% | -6.09%
\ No newline at end of file + 2m35.79s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m59.21s | 1549104 ko || -0m23.42s || -94408 ko | -13.06% | -6.09% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real.log.expected index 7e4cfaec1c..4864c1aaf7 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real.log.expected @@ -23,4 +23,4 @@ 0m27.81s | 756080 ko | Specific/NISTP256/AMD64/fenz | 0m28.91s | 756216 ko || -0m01.10s || -136 ko | -3.80% | -0.01% 0m22.81s | 766300 ko | Specific/X25519/C64/feadd | 0m23.43s | 766168 ko || -0m00.62s || 132 ko | -2.64% | +0.01% 0m11.15s | 687760 ko | Specific/X25519/C64/Synthesis | 0m11.23s | 687812 ko || -0m00.08s || -52 ko | -0.71% | -0.00% - 0m31.00s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m32.08s | 765212 ko || -0m01.07s || -4 ko | -3.36% | -0.00%
\ No newline at end of file + 0m31.00s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m32.08s | 765212 ko || -0m01.07s || -4 ko | -3.36% | -0.00% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-absolute.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-absolute.log.expected index ea116a804f..48e168657c 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-absolute.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-absolute.log.expected @@ -23,4 +23,4 @@ 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.72s | 648632 ko || -0m00.05s || -2332 ko | -2.90% | -0.35% 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.22s | 578344 ko || -0m00.04s || -3956 ko | -0.55% | -0.68% 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.58s | 546112 ko || +0m00.13s || -1940 ko | +8.86% | -0.35% - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12%
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-auto.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-auto.log.expected index 128f140662..fc26998b8f 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-auto.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-auto.log.expected @@ -23,4 +23,4 @@ 0m25.50s | 756080 ko | Specific/NISTP256/AMD64/fenz | 0m26.41s | 756216 ko || -0m00.91s || -136 ko | -3.44% | -0.01% 0m20.93s | 766300 ko | Specific/X25519/C64/feadd | 0m21.41s | 766168 ko || -0m00.48s || 132 ko | -2.24% | +0.01% 0m10.37s | 687760 ko | Specific/X25519/C64/Synthesis | 0m10.30s | 687812 ko || +0m00.06s || -52 ko | +0.67% | -0.00% - 0m28.51s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m29.46s | 765212 ko || -0m00.94s || -4 ko | -3.22% | -0.00%
\ No newline at end of file + 0m28.51s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m29.46s | 765212 ko || -0m00.94s || -4 ko | -3.22% | -0.00% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-diff.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-diff.log.expected index 79dc49892f..1fcdb84025 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-diff.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-diff.log.expected @@ -23,4 +23,4 @@ 0m39.59s | 793376 ko | Specific/NISTP256/AMD64/fesub | 0m40.09s | 799668 ko || -0m00.50s || -6292 ko | -1.24% | -0.78% 0m36.32s | 825448 ko | Specific/X25519/C64/femul | 0m39.50s | 839624 ko || -0m03.17s || -14176 ko | -8.05% | -1.68% 2m48.52s | 1589516 ko | Specific/solinas32_2e255m765_13limbs/femul | 3m12.95s | 1656912 ko || -0m24.42s || -67396 ko | -12.66% | -4.06% - 2m23.70s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m44.11s | 1549104 ko || -0m20.41s || -94408 ko | -12.43% | -6.09%
\ No newline at end of file + 2m23.70s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m44.11s | 1549104 ko || -0m20.41s || -94408 ko | -12.43% | -6.09% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user.log.expected index 128f140662..fc26998b8f 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user.log.expected @@ -23,4 +23,4 @@ 0m25.50s | 756080 ko | Specific/NISTP256/AMD64/fenz | 0m26.41s | 756216 ko || -0m00.91s || -136 ko | -3.44% | -0.01% 0m20.93s | 766300 ko | Specific/X25519/C64/feadd | 0m21.41s | 766168 ko || -0m00.48s || 132 ko | -2.24% | +0.01% 0m10.37s | 687760 ko | Specific/X25519/C64/Synthesis | 0m10.30s | 687812 ko || +0m00.06s || -52 ko | +0.67% | -0.00% - 0m28.51s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m29.46s | 765212 ko || -0m00.94s || -4 ko | -3.22% | -0.00%
\ No newline at end of file + 0m28.51s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m29.46s | 765212 ko || -0m00.94s || -4 ko | -3.22% | -0.00% diff --git a/test-suite/misc/redirect_printing.out b/test-suite/misc/redirect_printing.out new file mode 100644 index 0000000000..4f45c4d4c2 --- /dev/null +++ b/test-suite/misc/redirect_printing.out @@ -0,0 +1,2 @@ +nat_ind + : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n diff --git a/test-suite/misc/redirect_printing.sh b/test-suite/misc/redirect_printing.sh new file mode 100755 index 0000000000..7da17407f3 --- /dev/null +++ b/test-suite/misc/redirect_printing.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +$coqc misc/redirect_printing.v +diff -u redirect_test.out misc/redirect_printing.out diff --git a/test-suite/misc/redirect_printing.v b/test-suite/misc/redirect_printing.v new file mode 100644 index 0000000000..2f9096bcb8 --- /dev/null +++ b/test-suite/misc/redirect_printing.v @@ -0,0 +1,2 @@ +Set Printing Width 999999. +Redirect "redirect_test" Check nat_ind. diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index c4620f5b50..a3078af4a1 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -468,6 +468,7 @@ def make_table_string(stats_dict, for name in names]) def print_or_write_table(table, files): + if table[-1] != '\n': table += '\n' if len(files) == 0 or '-' in files: if hasattr(sys.stdout, 'buffer'): sys.stdout.buffer.write(table.encode("utf-8")) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 2d8734ff7f..a28d8f605b 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -404,6 +404,7 @@ let with_output_to_file fname func input = let channel = open_out (String.concat "." [fname; "out"]) in let old_fmt = !std_ft, !err_ft, !deep_ft in let new_ft = Format.formatter_of_out_channel channel in + set_gp new_ft (get_gp !std_ft); std_ft := new_ft; err_ft := new_ft; deep_ft := new_ft; @@ -412,6 +413,7 @@ let with_output_to_file fname func input = std_ft := Util.pi1 old_fmt; err_ft := Util.pi2 old_fmt; deep_ft := Util.pi3 old_fmt; + Format.pp_print_flush new_ft (); close_out channel; output with reraise -> @@ -419,6 +421,7 @@ let with_output_to_file fname func input = std_ft := Util.pi1 old_fmt; err_ft := Util.pi2 old_fmt; deep_ft := Util.pi3 old_fmt; + Format.pp_print_flush new_ft (); close_out channel; Exninfo.iraise reraise |