| 6cbbd2d | Jason Gross | 15 May 2021, 15:54:37 UTC | Add type.forall_each_lhs_of_arrow | 15 May 2021, 15:54:37 UTC |
| fbb9725 | Jason Gross | 15 May 2021, 01:37:36 UTC | Fix priorities to restore compat with fiat-crypto | 15 May 2021, 15:46:05 UTC |
| 611254f | Jason Gross | 13 May 2021, 21:30:50 UTC | Fix issue with previous commit | 15 May 2021, 15:46:05 UTC |
| 1f8c898 | Jason Gross | 13 May 2021, 21:01:42 UTC | Switch to a heterogenous `base_interp_beq` | 15 May 2021, 15:46:05 UTC |
| 6b0d525 | Jim Fehrle | 12 May 2021, 22:01:11 UTC | Overlay for coq/coq#14224 | 15 May 2021, 01:41:50 UTC |
| 4e0ebab | Jason Gross | 12 May 2021, 21:33:41 UTC | Add support for seprate ml files for Coq 8.14 | 12 May 2021, 21:33:41 UTC |
| dd1e74c | Jason Gross | 04 May 2021, 20:07:19 UTC | Switch to deprecated-hint-rewrite-without-locality Now we won't suppress warnings about non-rewrite hints | 04 May 2021, 20:07:19 UTC |
| 1749207 | Jason Gross | 30 April 2021, 14:28:23 UTC | Suppress some warnings when running coqc from not the root directory | 30 April 2021, 14:28:23 UTC |
| 6eee646 | Jason Gross | 27 April 2021, 21:53:18 UTC | Prove `wf_smart_App_curried` | 28 April 2021, 17:53:28 UTC |
| 468d209 | Jason Gross | 28 April 2021, 13:29:52 UTC | Regenerate _CoqProject.in | 28 April 2021, 13:29:52 UTC |
| dd34825 | Jason Gross | 28 April 2021, 13:29:34 UTC | Support PROFILE=1, better way of doing -deprecated-hint-without-locality | 28 April 2021, 13:29:34 UTC |
| 9842cc6 | Jason Gross | 28 April 2021, 13:15:54 UTC | Better GH Annotations | 28 April 2021, 13:16:02 UTC |
| b92757c | Jason Gross | 28 April 2021, 12:37:43 UTC | Suppress deprecated-hint-without-locality It's very noisy and there's no backwards compatible way to deal with it for `Hint Rewrite`, which does not support `Global` until very recent versions. | 28 April 2021, 12:38:22 UTC |
| 458b981 | Jason Gross | 27 April 2021, 19:55:28 UTC | Add some wf_reify aliases | 27 April 2021, 19:55:28 UTC |
| a8d0f31 | Jason Gross | 27 April 2021, 15:40:14 UTC | Don't hack around OTHERFLAGS See https://github.com/coq/coq/issues/10905#issuecomment-827707668 for some explanation, and note also that the hack I was using here meant that the rewriter would inherit OTHERFLAGS from the parent (e.g., fiat-crypto) make, which is not desired. | 27 April 2021, 15:40:14 UTC |
| e28c66c | Jason Gross | 27 April 2021, 15:26:35 UTC | Pass -native-compiler ondemand when it's supported Workaround for https://github.com/coq/coq/issues/14186 | 27 April 2021, 15:26:35 UTC |
| 0c2c317 | Jason Gross | 27 April 2021, 15:00:29 UTC | Prove `Wf <-> Wf3` We can be clever about how we're instantiating `var` types to carry enough information to ensure that variable uses line up. | 27 April 2021, 15:00:29 UTC |
| a132c21 | Jason Gross | 13 April 2021, 14:44:33 UTC | Update .gitignore with https://github.com/github/gitignore/pull/3701 | 13 April 2021, 14:44:33 UTC |
| 750b1a7 | Andrej Dudenhefner | 08 April 2021, 10:12:56 UTC | Future proof mod_bound_nonneg for https://github.com/coq/coq/pull/14086 | 09 April 2021, 11:20:01 UTC |
| ce996ca | Jason Gross | 24 March 2021, 21:30:31 UTC | notypeclasses in transparent assert Use `simple notypeclasses refine` in `transparent assert`. This was discovered in #23. The `notypeclasses` behavior is the one we want; even if the type is a typeclass, we want to leave over the corresponding goal. Closes #23. | 25 March 2021, 17:31:06 UTC |
| 766f449 | Jason Gross | 25 March 2021, 14:12:47 UTC | Fix typo | 25 March 2021, 14:12:47 UTC |
| 8a1b40e | Jason Gross | 25 March 2021, 14:12:12 UTC | Display GH Actions badge in Readme, now that Travis is gone | 25 March 2021, 14:12:12 UTC |
| a4525c7 | Jason Gross | 25 March 2021, 14:10:12 UTC | Switch from Travis CI to GH Actions Since Travis CI has been acquired, seems to have broken their promise, and is no longer a good service for OSS (c.f. https://www.jeffgeerling.com/blog/2020/travis-cis-new-pricing-plan-threw-wrench-my-open-source-works), we switch to GitHub actions. Files here are based on the fiat-crypto files | 25 March 2021, 14:10:12 UTC |
| ac6cb2f | Jason Gross | 10 February 2021, 15:32:06 UTC | Decrease upper bound on native tests For https://github.com/coq/coq/pull/13791#issuecomment-776781958 | 10 February 2021, 15:32:06 UTC |
| ace6ea0 | Hugo Herbelin | 20 November 2020, 07:38:37 UTC | Adapt to fixing dropped implicit arguments in Context. | 20 November 2020, 11:58:43 UTC |
| fe324e8 | Gaëtan Gilbert | 20 July 2020, 11:53:42 UTC | Adapt to coq/coq#12653 (syntax for cumulative inductives) | 18 November 2020, 15:27:02 UTC |
| 2ef7b66 | Jason Gross | 07 November 2020, 23:30:16 UTC | Update _CoqProject.in | 07 November 2020, 23:30:16 UTC |
| e1fc836 | Jason Gross | 06 November 2020, 01:26:25 UTC | Update warnings for master | 06 November 2020, 01:26:25 UTC |
| b2959f4 | Jason Gross | 06 November 2020, 01:10:55 UTC | Don't require a default argument for domain It wasn't actually particularly useful, and it's more convenient to not require two arguments. | 06 November 2020, 01:10:55 UTC |
| 7fca8d2 | Jason Gross | 04 November 2020, 23:10:02 UTC | Add CPS versions of expr inversion These are suitable for use in fixpoints which require guard-checker wrangling. | 04 November 2020, 23:10:35 UTC |
| fbfdbd9 | Jason Gross | 02 November 2020, 02:29:28 UTC | Revert "TEMP disable error redirection so we can see error messages on Mac" This reverts commit 180f6e205705a901a088c9e2f9e2d280bcf25e7c. | 02 November 2020, 02:29:28 UTC |
| 21b4442 | Jason Gross | 02 November 2020, 00:36:56 UTC | echo on Mac has no -n; thread_siblings_list doesn't exist | 02 November 2020, 00:36:56 UTC |
| 2a0a567 | Jason Gross | 02 November 2020, 00:29:58 UTC | Quote COQMF for Windows | 02 November 2020, 00:29:58 UTC |
| 180f6e2 | Jason Gross | 01 November 2020, 23:36:04 UTC | TEMP disable error redirection so we can see error messages on Mac | 01 November 2020, 23:36:04 UTC |
| ead9da0 | Jason Gross | 01 November 2020, 23:33:46 UTC | TEMP disable error redirection so we can see error messages on Windows | 01 November 2020, 23:33:46 UTC |
| 962d2e4 | Jason Gross | 01 November 2020, 21:51:22 UTC | Move back to f? parser notation We can do this with the resolution of https://github.com/coq/coq/issues/13281 by putting the notation at a higher level. | 01 November 2020, 21:51:22 UTC |
| 4ae25c5 | Jason Gross | 30 October 2020, 03:29:14 UTC | Add back a runtests_step_arg Mostly so that I can synchronize the harness between the three repos that are using it | 30 October 2020, 03:29:14 UTC |
| 3972006 | Jason Gross | 30 October 2020, 02:23:33 UTC | Fix for Coq 8.9 | 30 October 2020, 02:23:33 UTC |
| 122f6ae | Jason Gross | 29 October 2020, 02:57:40 UTC | Fix for Coq 8.9 We now parse Q expressions from strings manually rather than relying on Coq | 29 October 2020, 02:57:40 UTC |
| 921d6d7 | Jason Gross | 29 October 2020, 00:26:51 UTC | Update some equations for data | 29 October 2020, 00:26:51 UTC |
| c76ca80 | Jason Gross | 28 October 2020, 23:33:23 UTC | Improve perf data collection Ported from coq-community/coq-performance-tests | 28 October 2020, 23:34:41 UTC |
| 18dd8e3 | Jason Gross | 30 September 2020, 17:57:20 UTC | Multi-license under MIT OR Apache-2.0 OR BSD-1-Clause As per https://github.com/mit-plv/fiat-crypto/pull/881, since the rewriter code is effectively just a separate repo for part of the fiat-crypto project. | 30 September 2020, 17:57:20 UTC |
| 258a24b | Hugo Herbelin | 01 September 2020, 21:20:11 UTC | Adapting to Coq PR#12960: implicit arguments not any more lost when nesting two applicative notations. The code was relying on the implicit arguments being lost, so we need to add an explicit @ to preserve the previous behavior. | 02 September 2020, 20:41:37 UTC |
| e9b3505 | Jason Gross | 13 August 2020, 00:56:43 UTC | Finally, remove all uses of funext There were two insights that went into making it possible to remove functional extensionaliy. 1. The insight that went into 4d7999ebb66c1497222d024a1d9f9d0f1ecb2356: interp-relatedness implies equivalence. 2. Requiring `f x = v` in the `App`/`LetIn` case of `interp_related_gen` et al is essentially saying that, in order to prove `interp_related_gen`, we need to materialize an interpretation of the function part of applications. Since interpretation is in general highly non-trivial (for `rawexpr`s, `value`s, etc), we must weaken this condition. By instead only requiring `f x == v`, we only require being able to manifest *some* function which interprets to `v`, a much easier task. This weakening allows us to prove for each interpretation-relation `R` that `(exists e, R e v1 /\ R e v2) <-> v1 == v2`, i.e., that two interpreted values are equivalent iff there is some uninterpreted value which is related to both of them. Unfortunately this is not a full specification of interpretation-relatedness (we still need to say what it means for a particular uninterpreted value to be related to a particular interpreted value), and so we still end up doing a lot of work to prove various properties. <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) --------------------------------------------------------------------------------------------------------------------------------------------------------- 9m31.25s | 972156 ko | Total Time / Peak Mem | 8m49.94s | 955744 ko || +0m41.31s || 16412 ko | +7.79% | +1.71% --------------------------------------------------------------------------------------------------------------------------------------------------------- 1m14.56s | 859792 ko | Rewriter/Language/UnderLetsProofs | 0m46.66s | 767576 ko || +0m27.90s || 92216 ko | +59.79% | +12.01% 0m56.26s | 874108 ko | Rewriter/Rewriter/ProofsCommon | 0m48.79s | 869360 ko || +0m07.46s || 4748 ko | +15.31% | +0.54% 0m24.67s | 644504 ko | Rewriter/Language/Wf | 0m22.59s | 633232 ko || +0m02.08s || 11272 ko | +9.20% | +1.78% 1m04.38s | 953436 ko | Rewriter/Rewriter/InterpProofs | 1m03.09s | 955508 ko || +0m01.28s || -2072 ko | +2.04% | -0.21% 1m57.29s | 955812 ko | Rewriter/Rewriter/Wf | 1m57.19s | 955744 ko || +0m00.09s || 68 ko | +0.08% | +0.00% 0m38.73s | 972156 ko | Rewriter/Rewriter/Examples/SieveOfEratosthenes | 0m38.15s | 888496 ko || +0m00.57s || 83660 ko | +1.52% | +9.41% 0m34.85s | 811392 ko | Rewriter/Rewriter/Examples | 0m34.56s | 811664 ko || +0m00.28s || -272 ko | +0.83% | -0.03% 0m32.36s | 806524 ko | Rewriter/Rewriter/Examples/PrefixSums | 0m31.81s | 806696 ko || +0m00.55s || -172 ko | +1.72% | -0.02% 0m19.35s | 699656 ko | Rewriter/Rewriter/Examples/LiftLetsMap | 0m19.03s | 696620 ko || +0m00.32s || 3036 ko | +1.68% | +0.43% 0m18.74s | 612996 ko | Rewriter/Language/Inversion | 0m18.73s | 612420 ko || +0m00.00s || 576 ko | +0.05% | +0.09% 0m15.07s | 686200 ko | Rewriter/Rewriter/Examples/Plus0Tree | 0m14.93s | 685612 ko || +0m00.14s || 588 ko | +0.93% | +0.08% 0m14.94s | 685332 ko | Rewriter/Rewriter/Examples/UnderLetsPlus0 | 0m14.75s | 685192 ko || +0m00.18s || 140 ko | +1.28% | +0.02% 0m14.41s | 731276 ko | Rewriter/Demo | 0m14.43s | 743012 ko || -0m00.01s || -11736 ko | -0.13% | -1.57% 0m13.15s | 637292 ko | Rewriter/Language/IdentifiersLibraryProofs | 0m13.17s | 640980 ko || -0m00.01s || -3688 ko | -0.15% | -0.57% 0m06.79s | 503412 ko | Rewriter/Util/ListUtil | 0m06.56s | 501208 ko || +0m00.23s || 2204 ko | +3.50% | +0.43% 0m04.58s | 527384 ko | Rewriter/Language/IdentifiersBasicLibrary | 0m04.57s | 527564 ko || +0m00.00s || -180 ko | +0.21% | -0.03% 0m01.77s | 577488 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness | 0m01.87s | 577872 ko || -0m00.10s || -384 ko | -5.34% | -0.06% 0m01.72s | 457916 ko | Rewriter/Util/NatUtil | 0m01.70s | 457296 ko || +0m00.02s || 620 ko | +1.17% | +0.13% 0m01.55s | 521092 ko | Rewriter/Language/IdentifiersLibrary | 0m01.58s | 519796 ko || -0m00.03s || 1296 ko | -1.89% | +0.24% 0m01.34s | 518212 ko | Rewriter/Rewriter/Rewriter | 0m01.37s | 515708 ko || -0m00.03s || 2504 ko | -2.18% | +0.48% 0m01.22s | 518556 ko | Rewriter/Rewriter/Reify | 0m01.22s | 517588 ko || +0m00.00s || 968 ko | +0.00% | +0.18% 0m01.18s | 477976 ko | Rewriter/Language/Language | 0m01.15s | 477124 ko || +0m00.03s || 852 ko | +2.60% | +0.17% 0m01.14s | 539084 ko | Rewriter/Rewriter/AllTactics | 0m01.11s | 537084 ko || +0m00.02s || 2000 ko | +2.70% | +0.37% 0m01.13s | 444328 ko | Rewriter/Util/ListUtil/Forall | 0m01.04s | 445248 ko || +0m00.08s || -920 ko | +8.65% | -0.20% 0m00.95s | 523516 ko | Rewriter/Rewriter/ProofsCommonTactics | 0m00.95s | 520348 ko || +0m00.00s || 3168 ko | +0.00% | +0.60% 0m00.90s | 506864 ko | Rewriter/Language/IdentifiersGenerate | 0m00.81s | 505404 ko || +0m00.08s || 1460 ko | +11.11% | +0.28% 0m00.90s | 558172 ko | Rewriter/Rewriter/Examples/PerfTesting/All | 0m00.87s | 560168 ko || +0m00.03s || -1996 ko | +3.44% | -0.35% 0m00.89s | 532984 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings | 0m00.87s | 534512 ko || +0m00.02s || -1528 ko | +2.29% | -0.28% 0m00.83s | 507180 ko | Rewriter/Language/IdentifiersGenerateProofs | 0m00.84s | 506900 ko || -0m00.01s || 280 ko | -1.19% | +0.05% 0m00.82s | 530880 ko | Rewriter/Util/plugins/RewriterBuild | 0m00.79s | 529620 ko || +0m00.02s || 1260 ko | +3.79% | +0.23% 0m00.81s | 530028 ko | Rewriter/Util/plugins/RewriterBuildRegistry | 0m00.78s | 528980 ko || +0m00.03s || 1048 ko | +3.84% | +0.19% 0m00.78s | 533476 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports | 0m00.80s | 531528 ko || -0m00.02s || 1948 ko | -2.50% | +0.36% 0m00.70s | 458240 ko | Rewriter/Util/Bool/Reflect | 0m00.71s | 457920 ko || -0m00.01s || 320 ko | -1.40% | +0.06% 0m00.56s | 473820 ko | Rewriter/Language/IdentifiersBasicGenerate | 0m00.59s | 473848 ko || -0m00.02s || -28 ko | -5.08% | -0.00% 0m00.48s | 449072 ko | Rewriter/Util/MSetPositive/Facts | 0m00.47s | 449132 ko || +0m00.01s || -60 ko | +2.12% | -0.01% 0m00.46s | 463164 ko | Rewriter/Language/UnderLets | 0m00.46s | 462804 ko || +0m00.00s || 360 ko | +0.00% | +0.07% 0m00.31s | 400688 ko | Rewriter/Language/PreLemmas | 0m00.32s | 398084 ko || -0m00.01s || 2604 ko | -3.12% | +0.65% 0m00.27s | 312208 ko | Rewriter/Util/Option | 0m00.26s | 311880 ko || +0m00.01s || 328 ko | +3.84% | +0.10% 0m00.18s | 339048 ko | Rewriter/Util/OptionList | 0m00.17s | 338844 ko || +0m00.00s || 204 ko | +5.88% | +0.06% 0m00.09s | 202332 ko | Rewriter/Util/ListUtil/SetoidList | 0m00.12s | 202224 ko || -0m00.03s || 108 ko | -25.00% | +0.05% 0m00.08s | 133832 ko | Rewriter/Util/Bool | 0m00.08s | 116804 ko || +0m00.00s || 17028 ko | +0.00% | +14.57% 0m00.04s | 57244 ko | Rewriter/Util/Tactics/Contains | N/A | N/A || +0m00.04s || 57244 ko | ∞ | ∞ 0m00.03s | 58744 ko | Rewriter/Util/Tactics/SetoidSubst | N/A | N/A || +0m00.03s || 58744 ko | ∞ | ∞ ``` </p> | 16 August 2020, 23:17:03 UTC |
| 8c11afc | Jason Gross | 13 August 2020, 00:56:43 UTC | Add some tactics and instances This is in preparation for removing funext <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) --------------------------------------------------------------------------------------------------------------------------------------------------------- 8m47.72s | 972160 ko | Total Time / Peak Mem | 8m48.54s | 972292 ko || -0m00.82s || -132 ko | -0.15% | -0.01% --------------------------------------------------------------------------------------------------------------------------------------------------------- 0m36.93s | 972160 ko | Rewriter/Rewriter/Examples/SieveOfEratosthenes | 0m38.12s | 972292 ko || -0m01.18s || -132 ko | -3.12% | -0.01% 1m55.84s | 956436 ko | Rewriter/Rewriter/Wf | 1m56.36s | 955936 ko || -0m00.51s || 500 ko | -0.44% | +0.05% 1m02.44s | 955192 ko | Rewriter/Rewriter/InterpProofs | 1m02.10s | 952176 ko || +0m00.33s || 3016 ko | +0.54% | +0.31% 0m49.66s | 871776 ko | Rewriter/Rewriter/ProofsCommon | 0m49.37s | 871436 ko || +0m00.28s || 340 ko | +0.58% | +0.03% 0m46.64s | 769180 ko | Rewriter/Language/UnderLetsProofs | 0m46.64s | 766684 ko || +0m00.00s || 2496 ko | +0.00% | +0.32% 0m34.39s | 811424 ko | Rewriter/Rewriter/Examples | 0m34.45s | 811240 ko || -0m00.06s || 184 ko | -0.17% | +0.02% 0m31.59s | 806892 ko | Rewriter/Rewriter/Examples/PrefixSums | 0m31.91s | 806912 ko || -0m00.32s || -20 ko | -1.00% | -0.00% 0m22.70s | 636288 ko | Rewriter/Language/Wf | 0m22.71s | 603992 ko || -0m00.01s || 32296 ko | -0.04% | +5.34% 0m18.93s | 696488 ko | Rewriter/Rewriter/Examples/LiftLetsMap | 0m18.70s | 697788 ko || +0m00.23s || -1300 ko | +1.22% | -0.18% 0m18.75s | 612720 ko | Rewriter/Language/Inversion | 0m18.31s | 613016 ko || +0m00.44s || -296 ko | +2.40% | -0.04% 0m14.90s | 688488 ko | Rewriter/Rewriter/Examples/Plus0Tree | 0m14.92s | 684604 ko || -0m00.01s || 3884 ko | -0.13% | +0.56% 0m14.77s | 687744 ko | Rewriter/Rewriter/Examples/UnderLetsPlus0 | 0m14.84s | 690412 ko || -0m00.07s || -2668 ko | -0.47% | -0.38% 0m14.35s | 735844 ko | Rewriter/Demo | 0m14.46s | 741288 ko || -0m00.11s || -5444 ko | -0.76% | -0.73% 0m13.19s | 637012 ko | Rewriter/Language/IdentifiersLibraryProofs | 0m13.22s | 640668 ko || -0m00.03s || -3656 ko | -0.22% | -0.57% 0m06.83s | 503392 ko | Rewriter/Util/ListUtil | 0m06.76s | 506048 ko || +0m00.07s || -2656 ko | +1.03% | -0.52% 0m04.61s | 527308 ko | Rewriter/Language/IdentifiersBasicLibrary | 0m04.52s | 527564 ko || +0m00.09s || -256 ko | +1.99% | -0.04% 0m01.88s | 577004 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness | 0m01.83s | 577888 ko || +0m00.04s || -884 ko | +2.73% | -0.15% 0m01.68s | 458032 ko | Rewriter/Util/NatUtil | 0m01.72s | 457076 ko || -0m00.04s || 956 ko | -2.32% | +0.20% 0m01.56s | 519180 ko | Rewriter/Language/IdentifiersLibrary | 0m01.59s | 519968 ko || -0m00.03s || -788 ko | -1.88% | -0.15% 0m01.39s | 517952 ko | Rewriter/Rewriter/Rewriter | 0m01.38s | 517620 ko || +0m00.01s || 332 ko | +0.72% | +0.06% 0m01.25s | 518656 ko | Rewriter/Rewriter/Reify | 0m01.18s | 517984 ko || +0m00.07s || 672 ko | +5.93% | +0.12% 0m01.15s | 478092 ko | Rewriter/Language/Language | 0m01.15s | 477156 ko || +0m00.00s || 936 ko | +0.00% | +0.19% 0m01.14s | 538300 ko | Rewriter/Rewriter/AllTactics | 0m01.15s | 537684 ko || -0m00.01s || 616 ko | -0.86% | +0.11% 0m01.14s | 444184 ko | Rewriter/Util/ListUtil/Forall | 0m01.20s | 444240 ko || -0m00.06s || -56 ko | -5.00% | -0.01% 0m00.96s | 522016 ko | Rewriter/Rewriter/ProofsCommonTactics | 0m00.95s | 519928 ko || +0m00.01s || 2088 ko | +1.05% | +0.40% 0m00.88s | 557828 ko | Rewriter/Rewriter/Examples/PerfTesting/All | 0m00.88s | 556660 ko || +0m00.00s || 1168 ko | +0.00% | +0.20% 0m00.88s | 532552 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings | 0m00.90s | 531332 ko || -0m00.02s || 1220 ko | -2.22% | +0.22% 0m00.84s | 532444 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports | 0m00.83s | 532084 ko || +0m00.01s || 360 ko | +1.20% | +0.06% 0m00.83s | 506808 ko | Rewriter/Language/IdentifiersGenerate | 0m00.87s | 506684 ko || -0m00.04s || 124 ko | -4.59% | +0.02% 0m00.82s | 507288 ko | Rewriter/Language/IdentifiersGenerateProofs | 0m00.85s | 506916 ko || -0m00.03s || 372 ko | -3.52% | +0.07% 0m00.82s | 530212 ko | Rewriter/Util/plugins/RewriterBuild | 0m00.81s | 529172 ko || +0m00.00s || 1040 ko | +1.23% | +0.19% 0m00.80s | 529520 ko | Rewriter/Util/plugins/RewriterBuildRegistry | 0m00.77s | 528652 ko || +0m00.03s || 868 ko | +3.89% | +0.16% 0m00.69s | 458100 ko | Rewriter/Util/Bool/Reflect | 0m00.72s | 458264 ko || -0m00.03s || -164 ko | -4.16% | -0.03% 0m00.56s | 473620 ko | Rewriter/Language/IdentifiersBasicGenerate | 0m00.56s | 474056 ko || +0m00.00s || -436 ko | +0.00% | -0.09% 0m00.47s | 463448 ko | Rewriter/Language/UnderLets | 0m00.44s | 462932 ko || +0m00.02s || 516 ko | +6.81% | +0.11% 0m00.44s | 448948 ko | Rewriter/Util/MSetPositive/Facts | 0m00.47s | 448988 ko || -0m00.02s || -40 ko | -6.38% | -0.00% 0m00.32s | 400900 ko | Rewriter/Language/PreLemmas | 0m00.29s | 399556 ko || +0m00.03s || 1344 ko | +10.34% | +0.33% 0m00.26s | 312256 ko | Rewriter/Util/Option | 0m00.25s | 311884 ko || +0m00.01s || 372 ko | +4.00% | +0.11% 0m00.19s | 339012 ko | Rewriter/Util/OptionList | 0m00.17s | 338932 ko || +0m00.01s || 80 ko | +11.76% | +0.02% 0m00.12s | 202328 ko | Rewriter/Util/ListUtil/SetoidList | 0m00.13s | 202060 ko || -0m00.01s || 268 ko | -7.69% | +0.13% 0m00.08s | 133568 ko | Rewriter/Util/Bool | 0m00.07s | 116768 ko || +0m00.00s || 16800 ko | +14.28% | +14.38% 0m00.03s | 57532 ko | Rewriter/Util/Tactics/Contains | N/A | N/A || +0m00.03s || 57532 ko | ∞ | ∞ 0m00.03s | 58896 ko | Rewriter/Util/Tactics/SetoidSubst | N/A | N/A || +0m00.03s || 58896 ko | ∞ | ∞ ``` </p> | 16 August 2020, 22:58:44 UTC |
| 4856dc3 | Jason Gross | 13 August 2020, 16:24:57 UTC | Copy over list util lemmas from fiat-crypto | 13 August 2020, 16:24:57 UTC |
| 4d7999e | Jason Gross | 12 August 2020, 21:09:30 UTC | Progress on removing funext Using the insight that interp-relatedness implies equivalence, we can push the use of funext much further down. Unfortunately, the current use might be much harder to remove, as we effectively need to prove that interp-relatedness is proper with respect to type.eqv in its second argument. | 12 August 2020, 21:09:30 UTC |
| 0eb4fb6 | Jason Gross | 09 August 2020, 17:34:20 UTC | Test newer versions of Coq | 09 August 2020, 17:34:20 UTC |
| e7cada6 | Jason Gross | 15 July 2020, 23:08:08 UTC | Error for 'Not a truly recursive fixpoint' | 16 July 2020, 00:31:40 UTC |
| b470974 | Jason Gross | 15 July 2020, 22:54:30 UTC | deindent | 15 July 2020, 22:54:30 UTC |
| 61f32ce | Jason Gross | 15 July 2020, 22:33:28 UTC | Fix missing newline | 15 July 2020, 22:33:28 UTC |
| 67971fd | Jason Gross | 15 July 2020, 22:32:50 UTC | Mark more things as coq code | 15 July 2020, 22:32:50 UTC |
| b8e53ef | Jason Gross | 15 July 2020, 22:30:47 UTC | Add markdown description of the codebase | 15 July 2020, 22:30:55 UTC |
| 100e01c | Emilio Jesus Gallego Arias | 01 July 2020, 16:25:43 UTC | [coq] Adapt to coq/coq#11836 | 09 July 2020, 18:33:47 UTC |
| 97399a9 | Jason Gross | 29 June 2020, 19:06:00 UTC | Update _CoqProject.in | 29 June 2020, 19:06:00 UTC |
| ddfec55 | Jason Gross | 29 June 2020, 18:14:13 UTC | Also fatal error on omega-is-deprecated, now that we no longer use omega | 29 June 2020, 18:14:13 UTC |
| 9d9bcc2 | Jason Gross | 29 June 2020, 16:55:54 UTC | Fix for Coq v8.10 and earlier | 29 June 2020, 18:13:31 UTC |
| caa526f | Jason Gross | 29 June 2020, 16:21:17 UTC | Replace omega with lia The `omega` tactic is deprecated in new versions of Coq. <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) --------------------------------------------------------------------------------------------------------------------------------------------------------- 8m52.15s | 956024 ko | Total Time / Peak Mem | 8m43.86s | 956004 ko || +0m08.29s || 20 ko | +1.58% | +0.00% --------------------------------------------------------------------------------------------------------------------------------------------------------- 1m59.46s | 955892 ko | Rewriter/Rewriter/Wf | 1m56.08s | 955480 ko || +0m03.38s || 412 ko | +2.91% | +0.04% 1m02.72s | 956024 ko | Rewriter/Rewriter/InterpProofs | 1m02.69s | 956004 ko || +0m00.03s || 20 ko | +0.04% | +0.00% 0m48.84s | 868892 ko | Rewriter/Rewriter/ProofsCommon | 0m48.67s | 869796 ko || +0m00.17s || -904 ko | +0.34% | -0.10% 0m46.61s | 767016 ko | Rewriter/Language/UnderLetsProofs | 0m46.38s | 767348 ko || +0m00.22s || -332 ko | +0.49% | -0.04% 0m39.00s | 888416 ko | Rewriter/Rewriter/Examples/SieveOfEratosthenes | 0m38.05s | 888556 ko || +0m00.95s || -140 ko | +2.49% | -0.01% 0m35.33s | 812028 ko | Rewriter/Rewriter/Examples | 0m34.42s | 811640 ko || +0m00.90s || 388 ko | +2.64% | +0.04% 0m32.40s | 812368 ko | Rewriter/Rewriter/Examples/PrefixSums | 0m31.70s | 809164 ko || +0m00.69s || 3204 ko | +2.20% | +0.39% 0m22.57s | 633868 ko | Rewriter/Language/Wf | 0m22.06s | 633352 ko || +0m00.51s || 516 ko | +2.31% | +0.08% 0m19.32s | 696676 ko | Rewriter/Rewriter/Examples/LiftLetsMap | 0m18.89s | 696420 ko || +0m00.42s || 256 ko | +2.27% | +0.03% 0m18.73s | 612372 ko | Rewriter/Language/Inversion | 0m18.70s | 612488 ko || +0m00.03s || -116 ko | +0.16% | -0.01% 0m15.32s | 685284 ko | Rewriter/Rewriter/Examples/Plus0Tree | 0m14.87s | 685252 ko || +0m00.45s || 32 ko | +3.02% | +0.00% 0m15.10s | 685552 ko | Rewriter/Rewriter/Examples/UnderLetsPlus0 | 0m14.68s | 685316 ko || +0m00.41s || 236 ko | +2.86% | +0.03% 0m14.12s | 741332 ko | Rewriter/Demo | 0m14.42s | 745660 ko || -0m00.30s || -4328 ko | -2.08% | -0.58% 0m12.69s | 640980 ko | Rewriter/Language/IdentifiersLibraryProofs | 0m13.05s | 640948 ko || -0m00.36s || 32 ko | -2.75% | +0.00% 0m06.57s | 501448 ko | Rewriter/Util/ListUtil | 0m06.21s | 499796 ko || +0m00.36s || 1652 ko | +5.79% | +0.33% 0m04.43s | 527840 ko | Rewriter/Language/IdentifiersBasicLibrary | 0m04.59s | 527572 ko || -0m00.16s || 268 ko | -3.48% | +0.05% 0m01.87s | 577848 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness | 0m01.89s | 577352 ko || -0m00.01s || 496 ko | -1.05% | +0.08% 0m01.62s | 457404 ko | Rewriter/Util/NatUtil | 0m01.34s | 462232 ko || +0m00.28s || -4828 ko | +20.89% | -1.04% 0m01.56s | 519868 ko | Rewriter/Language/IdentifiersLibrary | 0m01.56s | 520084 ko || +0m00.00s || -216 ko | +0.00% | -0.04% 0m01.36s | 515684 ko | Rewriter/Rewriter/Rewriter | 0m01.28s | 515968 ko || +0m00.08s || -284 ko | +6.25% | -0.05% 0m01.22s | 517836 ko | Rewriter/Rewriter/Reify | 0m01.29s | 517768 ko || -0m00.07s || 68 ko | -5.42% | +0.01% 0m01.21s | 537252 ko | Rewriter/Rewriter/AllTactics | 0m01.10s | 537316 ko || +0m00.10s || -64 ko | +9.99% | -0.01% 0m01.15s | 477552 ko | Rewriter/Language/Language | 0m01.16s | 477224 ko || -0m00.01s || 328 ko | -0.86% | +0.06% 0m00.94s | 520056 ko | Rewriter/Rewriter/ProofsCommonTactics | 0m00.88s | 519996 ko || +0m00.05s || 60 ko | +6.81% | +0.01% 0m00.90s | 560264 ko | Rewriter/Rewriter/Examples/PerfTesting/All | 0m00.83s | 560480 ko || +0m00.07s || -216 ko | +8.43% | -0.03% 0m00.90s | 534680 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings | 0m00.85s | 534676 ko || +0m00.05s || 4 ko | +5.88% | +0.00% 0m00.88s | 527028 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports | 0m00.84s | 526908 ko || +0m00.04s || 120 ko | +4.76% | +0.02% 0m00.85s | 505752 ko | Rewriter/Language/IdentifiersGenerate | 0m00.85s | 505508 ko || +0m00.00s || 244 ko | +0.00% | +0.04% 0m00.83s | 506904 ko | Rewriter/Language/IdentifiersGenerateProofs | 0m00.85s | 506920 ko || -0m00.02s || -16 ko | -2.35% | -0.00% 0m00.82s | 529788 ko | Rewriter/Util/plugins/RewriterBuild | 0m00.82s | 532972 ko || +0m00.00s || -3184 ko | +0.00% | -0.59% 0m00.80s | 528672 ko | Rewriter/Util/plugins/RewriterBuildRegistry | 0m00.80s | 532352 ko || +0m00.00s || -3680 ko | +0.00% | -0.69% 0m00.70s | 457900 ko | Rewriter/Util/Bool/Reflect | 0m00.70s | 457084 ko || +0m00.00s || 816 ko | +0.00% | +0.17% 0m00.55s | 473748 ko | Rewriter/Language/IdentifiersBasicGenerate | 0m00.57s | 473808 ko || -0m00.01s || -60 ko | -3.50% | -0.01% 0m00.48s | 462984 ko | Rewriter/Language/UnderLets | 0m00.49s | 462976 ko || -0m00.01s || 8 ko | -2.04% | +0.00% 0m00.30s | 398428 ko | Rewriter/Language/PreLemmas | 0m00.30s | 397640 ko || +0m00.00s || 788 ko | +0.00% | +0.19% ``` </p> | 29 June 2020, 18:13:31 UTC |
| 5668def | Emilio Jesus Gallego Arias | 24 June 2020, 12:28:08 UTC | [coq] Adapt to coq/coq#12372 | 29 June 2020, 16:21:00 UTC |
| 1e47fca | Jason Gross | 21 June 2020, 03:05:31 UTC | Bump coq-scripts | 21 June 2020, 03:05:44 UTC |
| 821826e | Jason Gross | 21 June 2020, 02:43:43 UTC | Quiet a warning We no longer support Coq 8.7, so we don't need to reserve this notation, and it was giving: Warning: Notation "{ _ & _ }" was already defined with a different format. [notation-incompatible-format,parsing] | 21 June 2020, 02:43:43 UTC |
| 818069e | Jason Gross | 05 May 2020, 05:05:42 UTC | Add lemma missing from Coq 8.9 | 05 May 2020, 05:05:42 UTC |
| 5feaf0e | Jason Gross | 05 May 2020, 03:16:30 UTC | Add extra convenience lemmas | 05 May 2020, 03:16:30 UTC |
| 1a6956a | Jason Gross | 05 May 2020, 03:11:45 UTC | Fix previous commit | 05 May 2020, 03:11:45 UTC |
| e62d72a | Jason Gross | 05 May 2020, 03:10:08 UTC | Generalize lemmas a bit | 05 May 2020, 03:10:08 UTC |
| 8a644fe | Jason Gross | 05 May 2020, 02:47:01 UTC | Add more wf about App_curried | 05 May 2020, 02:47:01 UTC |
| d62dc8a | Jason Gross | 04 May 2020, 22:56:12 UTC | Don't auto-inline unit-typed definitions This is needed for preserving comments | 04 May 2020, 22:56:12 UTC |
| 0a99654 | Jason Gross | 04 May 2020, 22:55:51 UTC | Add some more inversion lemmas | 04 May 2020, 22:55:51 UTC |
| 677d3f2 | Jason Gross | 18 April 2020, 14:40:14 UTC | Add prove_Wf3 | 18 April 2020, 14:40:14 UTC |
| 6f9c96c | Jason Gross | 07 April 2020, 04:59:23 UTC | Add *.v.timing to .gitignore | 07 April 2020, 04:59:23 UTC |
| 7281c2f | Jason Gross | 06 April 2020, 02:24:13 UTC | Tell Coq to unfold Let_In later Turns out this is a bottleneck in fiat-crypto <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) --------------------------------------------------------------------------------------------------------------------------------------------------------- 8m46.11s | 972444 ko | Total Time / Peak Mem | 8m49.00s | 972408 ko || -0m02.89s || 36 ko | -0.54% | +0.00% --------------------------------------------------------------------------------------------------------------------------------------------------------- 1m55.01s | 956260 ko | Rewriter/Rewriter/Wf | 1m56.24s | 956040 ko || -0m01.23s || 220 ko | -1.05% | +0.02% 0m36.77s | 972444 ko | Rewriter/Rewriter/Examples/SieveOfEratosthenes | 0m38.03s | 972408 ko || -0m01.25s || 36 ko | -3.31% | +0.00% 1m02.22s | 956448 ko | Rewriter/Rewriter/InterpProofs | 1m02.89s | 956252 ko || -0m00.67s || 196 ko | -1.06% | +0.02% 0m48.66s | 873552 ko | Rewriter/Rewriter/ProofsCommon | 0m48.72s | 873796 ko || -0m00.06s || -244 ko | -0.12% | -0.02% 0m45.79s | 764632 ko | Rewriter/Language/UnderLetsProofs | 0m45.06s | 762548 ko || +0m00.72s || 2084 ko | +1.62% | +0.27% 0m34.50s | 811684 ko | Rewriter/Rewriter/Examples | 0m34.67s | 811864 ko || -0m00.17s || -180 ko | -0.49% | -0.02% 0m31.65s | 812932 ko | Rewriter/Rewriter/Examples/PrefixSums | 0m31.61s | 812836 ko || +0m00.03s || 96 ko | +0.12% | +0.01% 0m21.65s | 617796 ko | Rewriter/Language/Wf | 0m21.60s | 617808 ko || +0m00.04s || -12 ko | +0.23% | -0.00% 0m18.91s | 697856 ko | Rewriter/Rewriter/Examples/LiftLetsMap | 0m18.90s | 697992 ko || +0m00.01s || -136 ko | +0.05% | -0.01% 0m18.06s | 603992 ko | Rewriter/Language/Inversion | 0m18.33s | 603860 ko || -0m00.26s || 132 ko | -1.47% | +0.02% 0m15.01s | 685560 ko | Rewriter/Rewriter/Examples/Plus0Tree | 0m14.93s | 685668 ko || +0m00.08s || -108 ko | +0.53% | -0.01% 0m14.80s | 685540 ko | Rewriter/Rewriter/Examples/UnderLetsPlus0 | 0m14.77s | 685492 ko || +0m00.03s || 48 ko | +0.20% | +0.00% 0m14.33s | 746796 ko | Rewriter/Demo | 0m14.38s | 746668 ko || -0m00.05s || 128 ko | -0.34% | +0.01% 0m13.26s | 640904 ko | Rewriter/Language/IdentifiersLibraryProofs | 0m13.10s | 640936 ko || +0m00.16s || -32 ko | +1.22% | -0.00% 0m06.21s | 499380 ko | Rewriter/Util/ListUtil | 0m06.23s | 499120 ko || -0m00.02s || 260 ko | -0.32% | +0.05% 0m04.53s | 527184 ko | Rewriter/Language/IdentifiersBasicLibrary | 0m04.59s | 527184 ko || -0m00.05s || 0 ko | -1.30% | +0.00% 0m01.89s | 577984 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness | 0m01.86s | 577848 ko || +0m00.02s || 136 ko | +1.61% | +0.02% 0m01.57s | 519724 ko | Rewriter/Language/IdentifiersLibrary | 0m01.57s | 519612 ko || +0m00.00s || 112 ko | +0.00% | +0.02% 0m01.44s | 462452 ko | Rewriter/Util/NatUtil | 0m01.48s | 462488 ko || -0m00.04s || -36 ko | -2.70% | -0.00% 0m01.38s | 516000 ko | Rewriter/Rewriter/Rewriter | 0m01.35s | 515976 ko || +0m00.02s || 24 ko | +2.22% | +0.00% 0m01.27s | 517656 ko | Rewriter/Rewriter/Reify | 0m01.23s | 517468 ko || +0m00.04s || 188 ko | +3.25% | +0.03% 0m01.16s | 477004 ko | Rewriter/Language/Language | 0m01.15s | 477040 ko || +0m00.01s || -36 ko | +0.86% | -0.00% 0m01.07s | 536884 ko | Rewriter/Rewriter/AllTactics | 0m01.13s | 536988 ko || -0m00.05s || -104 ko | -5.30% | -0.01% 0m01.04s | 445048 ko | Rewriter/Util/ListUtil/Forall | 0m01.06s | 444992 ko || -0m00.02s || 56 ko | -1.88% | +0.01% 0m00.94s | 519888 ko | Rewriter/Rewriter/ProofsCommonTactics | 0m00.96s | 520152 ko || -0m00.02s || -264 ko | -2.08% | -0.05% 0m00.90s | 505712 ko | Rewriter/Language/IdentifiersGenerate | 0m00.88s | 505740 ko || +0m00.02s || -28 ko | +2.27% | -0.00% 0m00.88s | 560156 ko | Rewriter/Rewriter/Examples/PerfTesting/All | 0m00.92s | 560336 ko || -0m00.04s || -180 ko | -4.34% | -0.03% 0m00.87s | 534512 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings | 0m00.88s | 534632 ko || -0m00.01s || -120 ko | -1.13% | -0.02% 0m00.83s | 506752 ko | Rewriter/Language/IdentifiersGenerateProofs | 0m00.83s | 506832 ko || +0m00.00s || -80 ko | +0.00% | -0.01% 0m00.83s | 533120 ko | Rewriter/Util/plugins/RewriterBuild | 0m00.82s | 533120 ko || +0m00.01s || 0 ko | +1.21% | +0.00% 0m00.83s | 527300 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports | 0m00.85s | 526940 ko || -0m00.02s || 360 ko | -2.35% | +0.06% 0m00.80s | 532356 ko | Rewriter/Util/plugins/RewriterBuildRegistry | 0m00.79s | 531816 ko || +0m00.01s || 540 ko | +1.26% | +0.10% 0m00.73s | 457240 ko | Rewriter/Util/Bool/Reflect | 0m00.75s | 457312 ko || -0m00.02s || -72 ko | -2.66% | -0.01% 0m00.58s | 473952 ko | Rewriter/Language/IdentifiersBasicGenerate | 0m00.57s | 473668 ko || +0m00.01s || 284 ko | +1.75% | +0.05% 0m00.58s | 397164 ko | Rewriter/Util/Decidable | 0m00.55s | 397204 ko || +0m00.02s || -40 ko | +5.45% | -0.01% 0m00.48s | 463080 ko | Rewriter/Language/UnderLets | 0m00.49s | 463000 ko || -0m00.01s || 80 ko | -2.04% | +0.01% 0m00.41s | 449088 ko | Rewriter/Util/MSetPositive/Facts | 0m00.47s | 449104 ko || -0m00.06s || -16 ko | -12.76% | -0.00% 0m00.39s | 426348 ko | Rewriter/Util/MSetPositive/Equality | 0m00.39s | 426320 ko || +0m00.00s || 28 ko | +0.00% | +0.00% 0m00.36s | 397304 ko | Rewriter/Language/PreLemmas | 0m00.31s | 397460 ko || +0m00.04s || -156 ko | +16.12% | -0.03% 0m00.25s | 366084 ko | Rewriter/Util/FMapPositive/Equality | 0m00.30s | 365820 ko || -0m00.04s || 264 ko | -16.66% | +0.07% 0m00.24s | 311852 ko | Rewriter/Util/Option | 0m00.26s | 311840 ko || -0m00.02s || 12 ko | -7.69% | +0.00% 0m00.23s | 395224 ko | Rewriter/Util/Sum | 0m00.25s | 395172 ko || -0m00.01s || 52 ko | -7.99% | +0.01% 0m00.18s | 338884 ko | Rewriter/Util/OptionList | 0m00.18s | 338820 ko || +0m00.00s || 64 ko | +0.00% | +0.01% 0m00.14s | 191492 ko | Rewriter/Util/PrimitiveProd | 0m00.10s | 191564 ko || +0m00.04s || -72 ko | +40.00% | -0.03% 0m00.14s | 234688 ko | Rewriter/Util/Sigma | 0m00.16s | 234748 ko || -0m00.01s || -60 ko | -12.49% | -0.02% 0m00.11s | 202292 ko | Rewriter/Util/ListUtil/SetoidList | 0m00.14s | 202072 ko || -0m00.03s || 220 ko | -21.42% | +0.10% 0m00.11s | 187256 ko | Rewriter/Util/Prod | 0m00.09s | 187252 ko || +0m00.02s || 4 ko | +22.22% | +0.00% 0m00.10s | 136632 ko | Rewriter/Util/Equality | 0m00.09s | 136468 ko || +0m00.01s || 164 ko | +11.11% | +0.12% 0m00.10s | 150816 ko | Rewriter/Util/PrimitiveHList | 0m00.09s | 150872 ko || +0m00.01s || -56 ko | +11.11% | -0.03% 0m00.10s | 158752 ko | Rewriter/Util/PrimitiveSigma | 0m00.11s | 158792 ko || -0m00.00s || -40 ko | -9.09% | -0.02% 0m00.09s | 159012 ko | Rewriter/Language/Pre | 0m00.09s | 159120 ko || +0m00.00s || -108 ko | +0.00% | -0.06% 0m00.09s | 153284 ko | Rewriter/Language/PreCommon | 0m00.08s | 153232 ko || +0m00.00s || 52 ko | +12.49% | +0.03% 0m00.08s | 116644 ko | Rewriter/Util/Bool | 0m00.07s | 116456 ko || +0m00.00s || 188 ko | +14.28% | +0.16% 0m00.08s | 111908 ko | Rewriter/Util/Sigma/Related | 0m00.08s | 112120 ko || +0m00.00s || -212 ko | +0.00% | -0.18% 0m00.06s | 92892 ko | Rewriter/Util/LetIn | 0m00.04s | 93028 ko || +0m00.01s || -136 ko | +49.99% | -0.14% 0m00.06s | 72804 ko | Rewriter/Util/Tactics/DestructHead | 0m00.06s | 72752 ko || +0m00.00s || 52 ko | +0.00% | +0.07% 0m00.05s | 71136 ko | Rewriter/Util/CPSNotations | 0m00.04s | 71268 ko || +0m00.01s || -132 ko | +25.00% | -0.18% 0m00.05s | 87828 ko | Rewriter/Util/HProp | 0m00.06s | 87880 ko || -0m00.00s || -52 ko | -16.66% | -0.05% 0m00.05s | 76396 ko | Rewriter/Util/Notations | 0m00.05s | 76096 ko || +0m00.00s || 300 ko | +0.00% | +0.39% 0m00.04s | 67948 ko | Rewriter/Util/Bool/Equality | 0m00.04s | 67944 ko || +0m00.00s || 4 ko | +0.00% | +0.00% 0m00.04s | 78196 ko | Rewriter/Util/IffT | 0m00.06s | 78364 ko || -0m00.01s || -168 ko | -33.33% | -0.21% 0m00.04s | 60612 ko | Rewriter/Util/InductiveHList | 0m00.04s | 60588 ko || +0m00.00s || 24 ko | +0.00% | +0.03% 0m00.04s | 95540 ko | Rewriter/Util/Logic/ExistsEqAnd | 0m00.06s | 95728 ko || -0m00.01s || -188 ko | -33.33% | -0.19% 0m00.04s | 81808 ko | Rewriter/Util/Pointed | 0m00.05s | 81728 ko || -0m00.01s || 80 ko | -20.00% | +0.09% 0m00.04s | 59444 ko | Rewriter/Util/Tactics/CPSId | 0m00.03s | 59220 ko || +0m00.01s || 224 ko | +33.33% | +0.37% 0m00.04s | 57232 ko | Rewriter/Util/Tactics/EvarNormalize | 0m00.03s | 57232 ko || +0m00.01s || 0 ko | +33.33% | +0.00% 0m00.04s | 64852 ko | Rewriter/Util/Tactics/HeadUnderBinders | 0m00.03s | 64756 ko || +0m00.01s || 96 ko | +33.33% | +0.14% 0m00.04s | 57240 ko | Rewriter/Util/Tactics/PrintGoal | 0m00.04s | 57272 ko || +0m00.00s || -32 ko | +0.00% | -0.05% 0m00.04s | 83936 ko | Rewriter/Util/Tactics/RewriteHyp | 0m00.06s | 84016 ko || -0m00.01s || -80 ko | -33.33% | -0.09% 0m00.04s | 64520 ko | Rewriter/Util/Tactics/RunTacticAsConstr | 0m00.04s | 64368 ko || +0m00.00s || 152 ko | +0.00% | +0.23% 0m00.04s | 64452 ko | Rewriter/Util/Tactics/SpecializeAllWays | 0m00.03s | 64460 ko || +0m00.01s || -8 ko | +33.33% | -0.01% 0m00.04s | 65820 ko | Rewriter/Util/Tactics/SplitInContext | 0m00.03s | 65868 ko || +0m00.01s || -48 ko | +33.33% | -0.07% 0m00.04s | 57044 ko | Rewriter/Util/Tactics/Test | 0m00.02s | 56968 ko || +0m00.02s || 76 ko | +100.00% | +0.13% 0m00.03s | 71112 ko | Rewriter/Util/Comparison | 0m00.05s | 71192 ko || -0m00.02s || -80 ko | -40.00% | -0.11% 0m00.03s | 71080 ko | Rewriter/Util/FixCoqMistakes | 0m00.04s | 71144 ko || -0m00.01s || -64 ko | -25.00% | -0.08% 0m00.03s | 56756 ko | Rewriter/Util/GlobalSettings | 0m00.02s | 56852 ko || +0m00.00s || -96 ko | +49.99% | -0.16% 0m00.03s | 58416 ko | Rewriter/Util/Isomorphism | 0m00.04s | 58364 ko || -0m00.01s || 52 ko | -25.00% | +0.08% 0m00.03s | 77668 ko | Rewriter/Util/Logic/ProdForall | 0m00.04s | 77788 ko || -0m00.01s || -120 ko | -25.00% | -0.15% 0m00.03s | 68576 ko | Rewriter/Util/Tactics/BreakMatch | 0m00.02s | 68532 ko || +0m00.00s || 44 ko | +49.99% | +0.06% 0m00.03s | 59972 ko | Rewriter/Util/Tactics/CacheTerm | 0m00.03s | 59932 ko || +0m00.00s || 40 ko | +0.00% | +0.06% 0m00.03s | 64932 ko | Rewriter/Util/Tactics/DebugPrint | 0m00.03s | 64976 ko || +0m00.00s || -44 ko | +0.00% | -0.06% 0m00.03s | 66452 ko | Rewriter/Util/Tactics/DestructHyps | 0m00.03s | 66424 ko || +0m00.00s || 28 ko | +0.00% | +0.04% 0m00.03s | 64792 ko | Rewriter/Util/Tactics/DoWithHyp | 0m00.03s | 64736 ko || +0m00.00s || 56 ko | +0.00% | +0.08% 0m00.03s | 57100 ko | Rewriter/Util/Tactics/GetGoal | 0m00.03s | 57032 ko || +0m00.00s || 68 ko | +0.00% | +0.11% 0m00.03s | 64184 ko | Rewriter/Util/Tactics/Head | 0m00.03s | 64104 ko || +0m00.00s || 80 ko | +0.00% | +0.12% 0m00.03s | 57336 ko | Rewriter/Util/Tactics/PrintContext | 0m00.03s | 57296 ko || +0m00.00s || 40 ko | +0.00% | +0.06% 0m00.03s | 57184 ko | Rewriter/Util/Tactics/SetEvars | 0m00.04s | 57132 ko || -0m00.01s || 52 ko | -25.00% | +0.09% 0m00.03s | 65328 ko | Rewriter/Util/Tactics/SpecializeBy | 0m00.03s | 65320 ko || +0m00.00s || 8 ko | +0.00% | +0.01% 0m00.03s | 57052 ko | Rewriter/Util/Tactics/SubstEvars | 0m00.04s | 57060 ko || -0m00.01s || -8 ko | -25.00% | -0.01% 0m00.03s | 65020 ko | Rewriter/Util/Tactics/UniquePose | 0m00.03s | 64684 ko || +0m00.00s || 336 ko | +0.00% | +0.51% 0m00.03s | 59360 ko | Rewriter/Util/TypeList | 0m00.04s | 59228 ko || -0m00.01s || 132 ko | -25.00% | +0.22% 0m00.02s | 57316 ko | Rewriter/Util/Tactics/ConstrFail | 0m00.02s | 56988 ko || +0m00.00s || 328 ko | +0.00% | +0.57% 0m00.02s | 57200 ko | Rewriter/Util/Tactics/Not | 0m00.03s | 56960 ko || -0m00.00s || 240 ko | -33.33% | +0.42% 0m00.02s | 57860 ko | Rewriter/Util/Tactics/TransparentAssert | 0m00.04s | 57896 ko || -0m00.02s || -36 ko | -50.00% | -0.06% 0m00.02s | 57244 ko | Rewriter/Util/Tactics/WarnIfGoalsRemain | 0m00.03s | 57308 ko || -0m00.00s || -64 ko | -33.33% | -0.11% 0m00.02s | 56892 ko | Rewriter/Util/plugins/StrategyTactic | 0m00.02s | 56944 ko || +0m00.00s || -52 ko | +0.00% | -0.09% 0m00.01s | 64160 ko | Rewriter/Util/Tactics/AssertSucceedsPreserveError | 0m00.03s | 64324 ko || -0m00.01s || -164 ko | -66.66% | -0.25% ``` </p> | 06 April 2020, 03:07:04 UTC |
| c9b9756 | Jason Gross | 06 April 2020, 02:05:05 UTC | Make notations in expr_pat_scope only parsing | 06 April 2020, 02:05:05 UTC |
| 2c0e940 | Jason Gross | 06 April 2020, 00:32:39 UTC | Bump coq-scripts | 06 April 2020, 00:32:39 UTC |
| ddb7798 | Jason Gross | 30 March 2020, 01:37:59 UTC | Turn more warnings into errors Mostly just so that we don't backtrack on them | 30 March 2020, 01:38:16 UTC |
| d138f26 | Emilio Jesus Gallego Arias | 02 March 2020, 07:54:33 UTC | [coq] Adapt to coq/coq#11731 | 22 March 2020, 18:24:02 UTC |
| e073e09 | Jason Gross | 16 March 2020, 22:18:09 UTC | Remove etc/timeout | 16 March 2020, 22:18:09 UTC |
| b005fc6 | Jason Gross | 16 March 2020, 20:45:46 UTC | Add .gitattributes for windows checkout | 16 March 2020, 20:45:46 UTC |
| 39b45b2 | Pierre-Marie Pédrot | 09 March 2020, 08:29:19 UTC | Fix w.r.t. coq/coq#11764. | 11 March 2020, 01:09:13 UTC |
| 9667eef | Jason Gross | 10 March 2020, 01:29:28 UTC | Remove unused reserved notation that clashed with MSetInterface | 10 March 2020, 01:29:28 UTC |
| 54cf057 | Jason Gross | 26 February 2020, 04:15:53 UTC | Bump coq-scripts | 26 February 2020, 04:15:53 UTC |
| 40e83b3 | Jason Gross | 25 February 2020, 20:15:10 UTC | Fix broken perf machinery | 25 February 2020, 20:15:10 UTC |
| e0f867e | Jason Gross | 18 February 2020, 01:14:10 UTC | Add and{b_bool,}_for_each_lhs_of_arrow_Proper | 18 February 2020, 01:14:10 UTC |
| 3e51f06 | Jason Gross | 16 February 2020, 02:04:57 UTC | Bump coq-scripts for more robustness in timing logs | 16 February 2020, 02:04:57 UTC |
| 522d32d | Jason Gross | 14 February 2020, 22:34:01 UTC | Bump coq-scripts | 14 February 2020, 22:34:01 UTC |
| 536ad7d | Jason Gross | 14 February 2020, 03:18:08 UTC | More robust interp proofs in the presence of many let-ins | 14 February 2020, 03:18:08 UTC |
| 58469d2 | Jason Gross | 12 February 2020, 21:45:49 UTC | Improve error messages, start work on Demo.v | 12 February 2020, 21:45:49 UTC |
| 85e9e15 | Jason Gross | 31 January 2020, 22:32:10 UTC | Don't reduce the no-dtree versions early by default It costs too much memory in fiat-crypto. Incidentally, this should also get us back to basically the previous performance. Also, we now `Hint Opaque` constants in `wf`, to work around COQBUG(https://github.com/coq/coq/issues/11502) After | File Name | Before || Change | % Change ------------------------------------------------------------------------------------------------- 8m58.12s | Total | 10m43.22s || -1m45.10s | -16.34% ------------------------------------------------------------------------------------------------- 0m39.27s | Rewriter/Rewriter/Examples/SieveOfEratosthenes | 1m21.17s || -0m41.89s | -51.62% 0m31.91s | Rewriter/Rewriter/Examples/PrefixSums | 0m55.77s || -0m23.86s | -42.78% 0m34.61s | Rewriter/Rewriter/Examples | 0m49.45s || -0m14.84s | -30.01% 0m19.44s | Rewriter/Rewriter/Examples/LiftLetsMap | 0m33.83s || -0m14.38s | -42.53% 0m15.17s | Rewriter/Rewriter/Examples/Plus0Tree | 0m21.38s || -0m06.20s | -29.04% 0m15.09s | Rewriter/Rewriter/Examples/UnderLetsPlus0 | 0m20.68s || -0m05.58s | -27.03% 0m52.88s | Rewriter/Rewriter/ProofsCommon | 0m51.45s || +0m01.42s | +2.77% 2m00.04s | Rewriter/Rewriter/Wf | 2m00.25s || -0m00.20s | -0.17% 1m06.81s | Rewriter/Rewriter/InterpProofs | 1m06.79s || +0m00.01s | +0.02% 0m48.78s | Rewriter/Language/UnderLetsProofs | 0m48.60s || +0m00.17s | +0.37% 0m23.39s | Rewriter/Language/Wf | 0m23.48s || -0m00.08s | -0.38% 0m19.14s | Rewriter/Language/Inversion | 0m19.14s || +0m00.00s | +0.00% 0m13.68s | Rewriter/Language/IdentifiersLibraryProofs | 0m13.55s || +0m00.12s | +0.95% 0m06.48s | Rewriter/Util/ListUtil | 0m06.49s || -0m00.00s | -0.15% 0m04.73s | Rewriter/Language/IdentifiersBasicLibrary | 0m04.73s || +0m00.00s | +0.00% 0m01.96s | Rewriter/Rewriter/Examples/PerfTesting/Harness | 0m01.87s || +0m00.08s | +4.81% 0m01.67s | Rewriter/Language/IdentifiersLibrary | 0m01.71s || -0m00.04s | -2.33% 0m01.51s | Rewriter/Util/NatUtil | 0m01.60s || -0m00.09s | -5.62% 0m01.49s | Rewriter/Rewriter/Rewriter | 0m01.47s || +0m00.02s | +1.36% 0m01.35s | Rewriter/Rewriter/Reify | 0m01.37s || -0m00.02s | -1.45% 0m01.25s | Rewriter/Rewriter/AllTactics | 0m01.17s || +0m00.08s | +6.83% 0m01.24s | Rewriter/Util/ListUtil/Forall | 0m01.23s || +0m00.01s | +0.81% 0m01.23s | Rewriter/Language/Language | 0m01.24s || -0m00.01s | -0.80% 0m00.99s | Rewriter/Rewriter/Examples/PerfTesting/All | 0m00.94s || +0m00.05s | +5.31% 0m00.99s | Rewriter/Rewriter/ProofsCommonTactics | 0m01.02s || -0m00.03s | -2.94% 0m00.96s | Rewriter/Language/IdentifiersGenerate | 0m00.97s || -0m00.01s | -1.03% 0m00.96s | Rewriter/Language/IdentifiersGenerateProofs | 0m00.96s || +0m00.00s | +0.00% 0m00.93s | Rewriter/Rewriter/Examples/PerfTesting/Settings | 0m00.92s || +0m00.01s | +1.08% 0m00.90s | Rewriter/Util/plugins/RewriterBuildRegistry | 0m00.87s || +0m00.03s | +3.44% 0m00.86s | Rewriter/Util/plugins/RewriterBuild | 0m00.84s || +0m00.02s | +2.38% 0m00.84s | Rewriter/Util/plugins/RewriterBuildRegistryImports | 0m00.91s || -0m00.07s | -7.69% 0m00.75s | Rewriter/Util/Bool/Reflect | 0m00.78s || -0m00.03s | -3.84% 0m00.64s | Rewriter/Language/IdentifiersBasicGenerate | 0m00.61s || +0m00.03s | +4.91% 0m00.58s | Rewriter/Util/Decidable | 0m00.60s || -0m00.02s | -3.33% 0m00.52s | Rewriter/Language/UnderLets | 0m00.52s || +0m00.00s | +0.00% 0m00.52s | Rewriter/Util/MSetPositive/Facts | 0m00.45s || +0m00.07s | +15.55% 0m00.42s | Rewriter/Util/MSetPositive/Equality | 0m00.41s || +0m00.01s | +2.43% 0m00.33s | Rewriter/Language/PreLemmas | 0m00.36s || -0m00.02s | -8.33% 0m00.30s | Rewriter/Util/FMapPositive/Equality | 0m00.26s || +0m00.03s | +15.38% 0m00.29s | Rewriter/Util/Sum | 0m00.28s || +0m00.00s | +3.57% 0m00.27s | Rewriter/Util/Option | 0m00.30s || -0m00.02s | -9.99% 0m00.18s | Rewriter/Util/OptionList | 0m00.20s || -0m00.02s | -10.00% 0m00.17s | Rewriter/Util/Sigma | 0m00.17s || +0m00.00s | +0.00% 0m00.14s | Rewriter/Util/ListUtil/SetoidList | 0m00.14s || +0m00.00s | +0.00% 0m00.12s | Rewriter/Util/PrimitiveSigma | 0m00.11s || +0m00.00s | +9.09% 0m00.11s | Rewriter/Language/Pre | 0m00.11s || +0m00.00s | +0.00% 0m00.11s | Rewriter/Util/PrimitiveHList | 0m00.10s || +0m00.00s | +9.99% 0m00.10s | Rewriter/Util/Equality | 0m00.11s || -0m00.00s | -9.09% 0m00.10s | Rewriter/Util/PrimitiveProd | 0m00.11s || -0m00.00s | -9.09% 0m00.10s | Rewriter/Util/Prod | 0m00.11s || -0m00.00s | -9.09% 0m00.09s | Rewriter/Language/PreCommon | 0m00.07s || +0m00.01s | +28.57% 0m00.07s | Rewriter/Util/Bool | 0m00.05s || +0m00.02s | +40.00% 0m00.07s | Rewriter/Util/Logic/ExistsEqAnd | 0m00.05s || +0m00.02s | +40.00% 0m00.06s | Rewriter/Util/LetIn | 0m00.05s || +0m00.00s | +19.99% 0m00.06s | Rewriter/Util/Pointed | 0m00.05s || +0m00.00s | +19.99% 0m00.06s | Rewriter/Util/Sigma/Related | 0m00.05s || +0m00.00s | +19.99% 0m00.06s | Rewriter/Util/Tactics/DestructHead | 0m00.04s || +0m00.01s | +49.99% 0m00.05s | Rewriter/Util/Bool/Equality | 0m00.04s || +0m00.01s | +25.00% 0m00.05s | Rewriter/Util/IffT | 0m00.04s || +0m00.01s | +25.00% 0m00.05s | Rewriter/Util/Notations | 0m00.05s || +0m00.00s | +0.00% 0m00.05s | Rewriter/Util/Tactics/CacheTerm | 0m00.02s || +0m00.03s | +150.00% 0m00.05s | Rewriter/Util/Tactics/RewriteHyp | 0m00.04s || +0m00.01s | +25.00% 0m00.04s | Rewriter/Util/Comparison | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Rewriter/Util/FixCoqMistakes | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Rewriter/Util/GlobalSettings | 0m00.03s || +0m00.01s | +33.33% 0m00.04s | Rewriter/Util/HProp | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Rewriter/Util/InductiveHList | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Rewriter/Util/Logic/ProdForall | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Rewriter/Util/Tactics/AssertSucceedsPreserveError | 0m00.03s || +0m00.01s | +33.33% 0m00.04s | Rewriter/Util/Tactics/ConstrFail | 0m00.03s || +0m00.01s | +33.33% 0m00.04s | Rewriter/Util/Tactics/DebugPrint | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Rewriter/Util/Tactics/EvarNormalize | 0m00.02s || +0m00.02s | +100.00% 0m00.04s | Rewriter/Util/Tactics/HeadUnderBinders | 0m00.03s || +0m00.01s | +33.33% 0m00.04s | Rewriter/Util/Tactics/SpecializeBy | 0m00.02s || +0m00.02s | +100.00% 0m00.04s | Rewriter/Util/Tactics/UniquePose | 0m00.02s || +0m00.02s | +100.00% 0m00.04s | Rewriter/Util/Tactics/WarnIfGoalsRemain | 0m00.02s || +0m00.02s | +100.00% 0m00.03s | Rewriter/Util/CPSNotations | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/Tactics/BreakMatch | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/Tactics/CPSId | 0m00.03s || +0m00.00s | +0.00% 0m00.03s | Rewriter/Util/Tactics/GetGoal | 0m00.03s || +0m00.00s | +0.00% 0m00.03s | Rewriter/Util/Tactics/Head | 0m00.03s || +0m00.00s | +0.00% 0m00.03s | Rewriter/Util/Tactics/Not | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/Tactics/PrintGoal | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/Tactics/RunTacticAsConstr | 0m00.02s || +0m00.00s | +49.99% 0m00.03s | Rewriter/Util/Tactics/SetEvars | 0m00.03s || +0m00.00s | +0.00% 0m00.03s | Rewriter/Util/Tactics/SpecializeAllWays | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/Tactics/SplitInContext | 0m00.03s || +0m00.00s | +0.00% 0m00.03s | Rewriter/Util/Tactics/SubstEvars | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/Tactics/Test | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/Tactics/TransparentAssert | 0m00.03s || +0m00.00s | +0.00% 0m00.03s | Rewriter/Util/TypeList | 0m00.03s || +0m00.00s | +0.00% 0m00.02s | Rewriter/Util/Isomorphism | 0m00.03s || -0m00.00s | -33.33% 0m00.02s | Rewriter/Util/Tactics/DestructHyps | 0m00.02s || +0m00.00s | +0.00% 0m00.02s | Rewriter/Util/Tactics/DoWithHyp | 0m00.04s || -0m00.02s | -50.00% 0m00.02s | Rewriter/Util/Tactics/PrintContext | 0m00.03s || -0m00.00s | -33.33% 0m00.01s | Rewriter/Util/plugins/StrategyTactic | 0m00.03s || -0m00.01s | -66.66% | 08 February 2020, 05:34:56 UTC |
| 6ea1338 | Jason Gross | 27 January 2020, 23:45:02 UTC | Allow specifying more rewiter options We can now more easily disable use of pre-reduced constants, and can also more easily disable use of the decision tree. Unfortunately, this adds overhead in building the rewriter during the reduction phase. Not entirely sure what to do here. After | File Name | Before || Change | % Change ------------------------------------------------------------------------------------------------- 10m48.01s | Total | 8m59.98s || +1m48.02s | +20.00% ------------------------------------------------------------------------------------------------- 1m21.28s | Rewriter/Rewriter/Examples/SieveOfEratosthenes | 0m38.72s || +0m42.56s | +109.91% 0m57.91s | Rewriter/Rewriter/Examples/PrefixSums | 0m31.53s || +0m26.37s | +83.66% 0m49.54s | Rewriter/Rewriter/Examples | 0m34.10s || +0m15.43s | +45.27% 0m33.87s | Rewriter/Rewriter/Examples/LiftLetsMap | 0m18.91s || +0m14.95s | +79.11% 2m01.31s | Rewriter/Rewriter/Wf | 2m11.14s || -0m09.82s | -7.49% 0m21.26s | Rewriter/Rewriter/Examples/Plus0Tree | 0m14.82s || +0m06.44s | +43.45% 1m06.83s | Rewriter/Rewriter/InterpProofs | 1m01.77s || +0m05.05s | +8.19% 0m20.64s | Rewriter/Rewriter/Examples/UnderLetsPlus0 | 0m14.72s || +0m05.92s | +40.21% 0m52.61s | Rewriter/Rewriter/ProofsCommon | 0m51.98s || +0m00.63s | +1.21% 0m48.85s | Rewriter/Language/UnderLetsProofs | 0m49.10s || -0m00.25s | -0.50% 0m23.46s | Rewriter/Language/Wf | 0m23.45s || +0m00.01s | +0.04% 0m19.11s | Rewriter/Language/Inversion | 0m19.13s || -0m00.01s | -0.10% 0m13.57s | Rewriter/Language/IdentifiersLibraryProofs | 0m13.07s || +0m00.50s | +3.82% 0m06.45s | Rewriter/Util/ListUtil | 0m06.51s || -0m00.05s | -0.92% 0m04.73s | Rewriter/Language/IdentifiersBasicLibrary | 0m04.55s || +0m00.18s | +3.95% 0m01.97s | Rewriter/Rewriter/Examples/PerfTesting/Harness | 0m01.92s || +0m00.05s | +2.60% 0m01.67s | Rewriter/Language/IdentifiersLibrary | 0m01.66s || +0m00.01s | +0.60% 0m01.50s | Rewriter/Util/NatUtil | 0m01.53s || -0m00.03s | -1.96% 0m01.48s | Rewriter/Rewriter/Rewriter | 0m01.40s || +0m00.08s | +5.71% 0m01.35s | Rewriter/Rewriter/Reify | 0m01.35s || +0m00.00s | +0.00% 0m01.22s | Rewriter/Language/Language | 0m01.28s || -0m00.06s | -4.68% 0m01.22s | Rewriter/Rewriter/AllTactics | 0m01.07s || +0m00.14s | +14.01% 0m01.19s | Rewriter/Util/ListUtil/Forall | 0m01.18s || +0m00.01s | +0.84% 0m01.02s | Rewriter/Rewriter/ProofsCommonTactics | 0m01.03s || -0m00.01s | -0.97% 0m00.99s | Rewriter/Language/IdentifiersGenerate | 0m00.93s || +0m00.05s | +6.45% 0m00.97s | Rewriter/Rewriter/Examples/PerfTesting/All | 0m00.97s || +0m00.00s | +0.00% 0m00.95s | Rewriter/Language/IdentifiersGenerateProofs | 0m00.93s || +0m00.01s | +2.15% 0m00.94s | Rewriter/Rewriter/Examples/PerfTesting/Settings | 0m00.96s || -0m00.02s | -2.08% 0m00.87s | Rewriter/Util/plugins/RewriterBuild | 0m00.88s || -0m00.01s | -1.13% 0m00.86s | Rewriter/Util/plugins/RewriterBuildRegistry | 0m00.87s || -0m00.01s | -1.14% 0m00.86s | Rewriter/Util/plugins/RewriterBuildRegistryImports | 0m00.86s || +0m00.00s | +0.00% 0m00.76s | Rewriter/Util/Bool/Reflect | 0m00.76s || +0m00.00s | +0.00% 0m00.64s | Rewriter/Language/IdentifiersBasicGenerate | 0m00.61s || +0m00.03s | +4.91% 0m00.55s | Rewriter/Util/Decidable | 0m00.61s || -0m00.05s | -9.83% 0m00.49s | Rewriter/Language/UnderLets | 0m00.51s || -0m00.02s | -3.92% 0m00.48s | Rewriter/Util/MSetPositive/Facts | 0m00.48s || +0m00.00s | +0.00% 0m00.42s | Rewriter/Util/MSetPositive/Equality | 0m00.45s || -0m00.03s | -6.66% 0m00.37s | Rewriter/Language/PreLemmas | 0m00.38s || -0m00.01s | -2.63% 0m00.31s | Rewriter/Util/Sum | 0m00.29s || +0m00.02s | +6.89% 0m00.27s | Rewriter/Util/Option | 0m00.27s || +0m00.00s | +0.00% 0m00.25s | Rewriter/Util/FMapPositive/Equality | 0m00.26s || -0m00.01s | -3.84% 0m00.21s | Rewriter/Util/OptionList | 0m00.20s || +0m00.00s | +4.99% 0m00.16s | Rewriter/Util/Sigma | 0m00.17s || -0m00.01s | -5.88% 0m00.12s | Rewriter/Util/ListUtil/SetoidList | 0m00.15s || -0m00.03s | -20.00% 0m00.11s | Rewriter/Language/PreCommon | 0m00.09s || +0m00.02s | +22.22% 0m00.11s | Rewriter/Util/PrimitiveProd | 0m00.13s || -0m00.02s | -15.38% 0m00.10s | Rewriter/Util/Equality | 0m00.10s || +0m00.00s | +0.00% 0m00.10s | Rewriter/Util/PrimitiveHList | 0m00.09s || +0m00.01s | +11.11% 0m00.10s | Rewriter/Util/PrimitiveSigma | 0m00.11s || -0m00.00s | -9.09% 0m00.09s | Rewriter/Language/Pre | 0m00.11s || -0m00.02s | -18.18% 0m00.09s | Rewriter/Util/Prod | 0m00.11s || -0m00.02s | -18.18% 0m00.09s | Rewriter/Util/Sigma/Related | 0m00.07s || +0m00.01s | +28.57% 0m00.08s | Rewriter/Util/Bool | 0m00.08s || +0m00.00s | +0.00% 0m00.06s | Rewriter/Util/FixCoqMistakes | 0m00.04s || +0m00.01s | +49.99% 0m00.06s | Rewriter/Util/HProp | 0m00.07s || -0m00.01s | -14.28% 0m00.06s | Rewriter/Util/Logic/ExistsEqAnd | 0m00.07s || -0m00.01s | -14.28% 0m00.06s | Rewriter/Util/Notations | 0m00.05s || +0m00.00s | +19.99% 0m00.06s | Rewriter/Util/Pointed | 0m00.05s || +0m00.00s | +19.99% 0m00.05s | Rewriter/Util/IffT | 0m00.05s || +0m00.00s | +0.00% 0m00.05s | Rewriter/Util/LetIn | 0m00.05s || +0m00.00s | +0.00% 0m00.05s | Rewriter/Util/Tactics/BreakMatch | 0m00.05s || +0m00.00s | +0.00% 0m00.05s | Rewriter/Util/Tactics/RewriteHyp | 0m00.05s || +0m00.00s | +0.00% 0m00.05s | Rewriter/Util/Tactics/TransparentAssert | 0m00.04s || +0m00.01s | +25.00% 0m00.04s | Rewriter/Util/Bool/Equality | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Rewriter/Util/CPSNotations | 0m00.03s || +0m00.01s | +33.33% 0m00.04s | Rewriter/Util/Tactics/ConstrFail | 0m00.03s || +0m00.01s | +33.33% 0m00.04s | Rewriter/Util/Tactics/DebugPrint | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Rewriter/Util/Tactics/DestructHyps | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Rewriter/Util/Tactics/DoWithHyp | 0m00.03s || +0m00.01s | +33.33% 0m00.04s | Rewriter/Util/Tactics/EvarNormalize | 0m00.02s || +0m00.02s | +100.00% 0m00.04s | Rewriter/Util/Tactics/HeadUnderBinders | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Rewriter/Util/Tactics/Not | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Rewriter/Util/Tactics/RunTacticAsConstr | 0m00.03s || +0m00.01s | +33.33% 0m00.04s | Rewriter/Util/Tactics/SetEvars | 0m00.02s || +0m00.02s | +100.00% 0m00.04s | Rewriter/Util/Tactics/SpecializeAllWays | 0m00.05s || -0m00.01s | -20.00% 0m00.04s | Rewriter/Util/Tactics/SubstEvars | 0m00.02s || +0m00.02s | +100.00% 0m00.03s | Rewriter/Util/Comparison | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/GlobalSettings | 0m00.05s || -0m00.02s | -40.00% 0m00.03s | Rewriter/Util/InductiveHList | 0m00.03s || +0m00.00s | +0.00% 0m00.03s | Rewriter/Util/Logic/ProdForall | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/Tactics/AssertSucceedsPreserveError | 0m00.03s || +0m00.00s | +0.00% 0m00.03s | Rewriter/Util/Tactics/CPSId | 0m00.03s || +0m00.00s | +0.00% 0m00.03s | Rewriter/Util/Tactics/CacheTerm | 0m00.02s || +0m00.00s | +49.99% 0m00.03s | Rewriter/Util/Tactics/DestructHead | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/Tactics/GetGoal | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/Tactics/PrintContext | 0m00.02s || +0m00.00s | +49.99% 0m00.03s | Rewriter/Util/Tactics/PrintGoal | 0m00.02s || +0m00.00s | +49.99% 0m00.03s | Rewriter/Util/Tactics/SpecializeBy | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/Tactics/SplitInContext | 0m00.05s || -0m00.02s | -40.00% 0m00.03s | Rewriter/Util/Tactics/UniquePose | 0m00.04s || -0m00.01s | -25.00% 0m00.03s | Rewriter/Util/Tactics/WarnIfGoalsRemain | 0m00.03s || +0m00.00s | +0.00% 0m00.03s | Rewriter/Util/TypeList | 0m00.03s || +0m00.00s | +0.00% 0m00.02s | Rewriter/Util/Isomorphism | 0m00.04s || -0m00.02s | -50.00% 0m00.02s | Rewriter/Util/Tactics/Head | 0m00.03s || -0m00.00s | -33.33% 0m00.02s | Rewriter/Util/Tactics/Test | 0m00.03s || -0m00.00s | -33.33% 0m00.02s | Rewriter/Util/plugins/StrategyTactic | 0m00.04s || -0m00.02s | -50.00% | 08 February 2020, 05:34:56 UTC |
| bb4cd1a | Jason Gross | 06 February 2020, 06:49:15 UTC | Mark all constants as opaque in wf and interp dbs | 07 February 2020, 21:03:41 UTC |
| 401a1d1 | Jason Gross | 06 February 2020, 06:28:18 UTC | Add opacity information to hint databases This should hopefully make some things faster | 06 February 2020, 06:32:03 UTC |
| 96b0aba | Jason Gross | 06 February 2020, 06:26:34 UTC | Bump coq-scripts | 06 February 2020, 06:26:40 UTC |
| 832dab3 | Jason Gross | 27 January 2020, 22:25:11 UTC | Allow skipping early reduction Useful for debugging and eventually for perf-testing the effect of pattern matching compilation. | 27 January 2020, 22:25:11 UTC |
| 67e832e | Jason Gross | 23 January 2020, 18:53:30 UTC | Make clean target work when upgrading to Coq 8.10 Fixes #4 | 23 January 2020, 18:53:30 UTC |
| 0ddd54f | Hugo Herbelin | 19 January 2020, 20:12:37 UTC | Adapting to Coq PR #11135: local declarations of primitive records kept folded. As a consequence, an extra unfold is needed somewhere. The added unfold preserves backward compatibility. | 20 January 2020, 09:10:26 UTC |
| 0860836 | Jason Gross | 20 January 2020, 03:34:58 UTC | Fix .travis.yml after a recent change to Travis broke the build | 20 January 2020, 03:34:58 UTC |
| 61c6b7c | Gaëtan Gilbert | 16 December 2019, 11:00:57 UTC | Adapt to coq/coq#11027 (cleanup comind interface) | 18 December 2019, 23:04:14 UTC |
| 27d6bfd | Jason Gross | 28 November 2019, 20:35:19 UTC | Remove dead code It was breaking https://github.com/coq/coq/pull/11029 | 28 November 2019, 20:35:19 UTC |
| c8117a0 | Jason Gross | 27 November 2019, 22:01:38 UTC | Ship a multi-version _CoqProject replacement | 27 November 2019, 22:01:38 UTC |
| 3d99561 | Jason Gross | 27 November 2019, 18:40:30 UTC | Fix build | 27 November 2019, 18:40:30 UTC |
| ba9c01b | Jason Gross | 27 November 2019, 16:07:15 UTC | Sort _CoqProject before comparing We don't need to update it if it's just the order that's changed | 27 November 2019, 16:07:15 UTC |
