a7e88a2 | Jason Gross | 10 August 2022, 18:12:06 UTC | Fix check-all run | 10 August 2022, 18:12:06 UTC |
6c69287 | Jason Gross | 27 July 2022, 00:53:48 UTC | Add an example dealing with defined constants (#53) | 27 July 2022, 00:53:48 UTC |
7c23e6e | Jason Gross | 27 July 2022, 00:19:11 UTC | Split off Reify.v (#52) For ease of changes without rebuilding everything | 27 July 2022, 00:19:11 UTC |
307ae3f | Jason Gross | 26 July 2022, 22:22:43 UTC | Clear unused deps in `cache_term` for `transparent_abstract` (#51) | 26 July 2022, 22:22:43 UTC |
7fe56c3 | Jason Gross | 26 July 2022, 20:24:41 UTC | Remove some unused requires (#50) | 26 July 2022, 20:24:41 UTC |
369f019 | Jason Gross | 26 July 2022, 20:11:01 UTC | Rename build to build-dev for clarity of branch protection | 26 July 2022, 20:11:01 UTC |
50a7857 | Jason Gross | 26 July 2022, 20:09:03 UTC | Add check-all for ease of automatic checking of CI | 26 July 2022, 20:09:03 UTC |
79e7573 | Jason Gross | 26 July 2022, 16:25:16 UTC | Don't leave over a useless let-in in `cache_term` (#49) | 26 July 2022, 16:25:16 UTC |
474c44b | dependabot[bot] | 15 July 2022, 15:47:29 UTC | Bump etc/coq-scripts from `d85c149` to `5116cc9` (#47) | 15 July 2022, 15:47:29 UTC |
f3f6bc1 | dependabot[bot] | 03 July 2022, 02:56:53 UTC | Bump etc/coq-scripts from `3be05c7` to `d85c149` (#46) | 03 July 2022, 02:56:53 UTC |
3915f16 | Jason Gross | 01 July 2022, 01:16:08 UTC | Drop support for Coq < 8.11, make hint globality explicit (#45) This is mostly an adaptation for coq/coq#16004 We also make some other warnings into errors at the same time. | 01 July 2022, 01:16:08 UTC |
f18f187 | dependabot[bot] | 13 June 2022, 17:09:23 UTC | Bump etc/coq-scripts from `0ca86bb` to `d85c149` (#44) | 13 June 2022, 17:09:23 UTC |
f667a10 | Jason Gross | 13 June 2022, 16:35:46 UTC | Bump ocaml version on docker-coq CI See https://github.com/fblanqui/color/pull/42#issuecomment-1141247333 and https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs-.26-users/topic/coq.3Adev.20Docker.20tag.20currently.20unavailable/near/282503558 | 13 June 2022, 16:35:46 UTC |
2c2d78e | dependabot[bot] | 28 March 2022, 16:41:00 UTC | Bump etc/coq-scripts from `7e68a28` to `0ca86bb` (#40) | 28 March 2022, 16:41:00 UTC |
10c6a00 | dependabot[bot] | 17 March 2022, 22:03:44 UTC | Bump etc/coq-scripts from `3be05c7` to `7e68a28` (#39) | 17 March 2022, 22:03:44 UTC |
3fc0c44 | dependabot[bot] | 02 March 2022, 19:00:06 UTC | Bump actions/checkout from 2 to 3 (#38) Bumps [actions/checkout](https://github.com/actions/checkout) from 2 to 3. - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](https://github.com/actions/checkout/compare/v2...v3) --- updated-dependencies: - dependency-name: actions/checkout dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> | 02 March 2022, 19:00:06 UTC |
5ca81b1 | Jason Gross | 10 February 2022, 07:15:13 UTC | Ignore newly generated file | 10 February 2022, 07:15:13 UTC |
2bd8776 | Enrico Tassi | 03 February 2022, 20:29:15 UTC | adapt to coq/coq#15220 (#34) | 03 February 2022, 20:29:15 UTC |
73192bd | Jason Gross | 26 January 2022, 20:34:14 UTC | Update _CoqProject | 26 January 2022, 20:34:14 UTC |
8278f35 | Jason Gross | 26 January 2022, 19:50:44 UTC | Add Tactics.FindHyp, fix bug in unique pose Work around https://github.com/coq/coq/issues/15554 | 26 January 2022, 19:50:44 UTC |
629c4f4 | Jason Gross | 13 January 2022, 23:48:17 UTC | Add util lemmas ported from fiat-crypto (#37) Just to keep these files up to date with the versions in fiat-crypto | 13 January 2022, 23:48:17 UTC |
d5edc92 | dependabot[bot] | 16 December 2021, 16:14:01 UTC | Merge pull request #36 from mit-plv/dependabot/submodules/etc/coq-scripts-3be05c7 | 16 December 2021, 16:14:01 UTC |
f03b6f0 | dependabot[bot] | 16 December 2021, 15:23:28 UTC | Bump etc/coq-scripts from `c34a5e9` to `3be05c7` Bumps [etc/coq-scripts](https://github.com/JasonGross/coq-scripts) from `c34a5e9` to `3be05c7`. - [Release notes](https://github.com/JasonGross/coq-scripts/releases) - [Commits](https://github.com/JasonGross/coq-scripts/compare/c34a5e9f645a5aac30fbf175732791797bcf18a2...3be05c7888f95f106ab4a637b3e354fd2cf3a783) --- updated-dependencies: - dependency-name: etc/coq-scripts dependency-type: direct:production ... Signed-off-by: dependabot[bot] <support@github.com> | 16 December 2021, 15:23:28 UTC |
fc3a1d6 | dependabot[bot] | 16 December 2021, 03:24:11 UTC | Merge pull request #35 from mit-plv/dependabot/submodules/etc/coq-scripts-c34a5e9 | 16 December 2021, 03:24:11 UTC |
29d1a26 | dependabot[bot] | 15 December 2021, 23:30:46 UTC | Bump etc/coq-scripts from `1ad4075` to `c34a5e9` Bumps [etc/coq-scripts](https://github.com/JasonGross/coq-scripts) from `1ad4075` to `c34a5e9`. - [Release notes](https://github.com/JasonGross/coq-scripts/releases) - [Commits](https://github.com/JasonGross/coq-scripts/compare/1ad4075c553415ba01f27796231ef26019e76093...c34a5e9f645a5aac30fbf175732791797bcf18a2) --- updated-dependencies: - dependency-name: etc/coq-scripts dependency-type: direct:production ... Signed-off-by: dependabot[bot] <support@github.com> | 15 December 2021, 23:30:46 UTC |
60cfea5 | Jason Gross | 15 December 2021, 23:30:29 UTC | Update dependabot.yml Add submodule support | 15 December 2021, 23:30:29 UTC |
dbc67ab | Jason Gross | 16 November 2021, 18:35:37 UTC | Don't duplicate inclusion of Makefile.local-late | 16 November 2021, 18:35:37 UTC |
55cf842 | Jason Gross | 11 November 2021, 22:20:31 UTC | [CI] Update Coq versions | 13 November 2021, 10:31:32 UTC |
0e5f243 | Jason Gross | 08 November 2021, 01:24:23 UTC | [ci] better submodules init | 08 November 2021, 01:24:23 UTC |
42c6f3c | Jason Gross | 08 November 2021, 01:22:27 UTC | Create dependabot.yml | 08 November 2021, 01:22:27 UTC |
a038b7c | Pierre-Marie Pédrot | 20 September 2021, 20:34:08 UTC | Adapt w.r.t. coq/coq#14903. | 23 September 2021, 02:06:36 UTC |
eae3592 | Jason Gross | 22 September 2021, 18:49:53 UTC | [ci] [docker] chmod recursively | 22 September 2021, 18:49:53 UTC |
74b7f34 | Jason Gross | 22 September 2021, 18:41:00 UTC | [ci] Install extra deps on docker | 22 September 2021, 18:41:00 UTC |
1296003 | Hugo Herbelin | 09 September 2021, 22:08:19 UTC | Adapting to Coq PR #14711: Evd.check_univ_decl returns also the universe binders. | 21 September 2021, 15:39:37 UTC |
0f5d4a2 | Jason Gross | 15 September 2021, 01:42:11 UTC | [CI] Fix custom_script usage | 15 September 2021, 01:42:11 UTC |
91a8857 | Jason Gross | 15 September 2021, 01:37:02 UTC | Move master build to docker-coq action This way we don't have to wait for the ppa to update to rebuild PRs to be merged synchronously with Coq. | 15 September 2021, 01:38:09 UTC |
83bb7c4 | Jason Gross | 10 September 2021, 19:44:35 UTC | Add support for seprate ml files for Coq 8.15 ``` ( export v=814; bash -c "for i in \$(git ls-files '*.v${v}'); do cp \$i \${i/v${v}/v$((${v}+1))}; git add \${i/v${v}/v$((${v}+1))}; done" ) ``` or ``` for i in $(git ls-files "*.v814"); do cp $i ${i/v814/v815}; git add ${i/v814/v815}; done ``` | 11 September 2021, 04:11:58 UTC |
e3a767a | Jason Gross | 16 July 2021, 22:47:56 UTC | Fix stack overflow on examples | 16 July 2021, 22:50:58 UTC |
411a43e | Jason Gross | 16 July 2021, 15:33:39 UTC | Prefix with List. for compat with Coq <= 8.10 | 16 July 2021, 15:33:39 UTC |
5347625 | Jason Gross | 15 July 2021, 15:08:41 UTC | Restore old version of perf-testing data sampling I don't want to change the data sampling method right now for the paper, so I'm reverting to the density of data collection that we were previously using. | 15 July 2021, 15:08:41 UTC |
7553a6d | Jason Gross | 26 May 2021, 19:24:57 UTC | Get rid of dead code in gh-actions make _CoqProject is now generated | 26 May 2021, 19:24:57 UTC |
493170e | Hugo Herbelin | 24 May 2021, 15:21:53 UTC | Reserved Infix "'o'" used to reserve "'o'"; with Coq's #14379, it reserves "o". We remove the notation which was not used. If really needed as it was, it should be written « Reserved Infix "''o''" ». | 24 May 2021, 15:58:10 UTC |
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 |