HEAD | 19f344b | speedup wf{3,4}_of_wf by factorizing raw matches to definitions (#157) This greatly reduces term size (tree size 1988106 -> 1121651 for wf3_of_wf). Timings before: (Succeed Qed includes some time which isn't in Time Qed, see also https://github.com/coq/coq/pull/19426) wf3 tactics 2.2s qed 1.09s succeed qed 1.25s wf4 tactics 14.5s qed 7.4s succeed qed 8.5s After: wf3 tactics 1.4s qed 0.6s succeed qed 0.65s wf4 tactics 8s qed 3.6s succeed qed 4s | 29 July 2024, 21:55:44 UTC |
refs/heads/ITP-2022-perf-data | 1787ab4 | Revert "Remake perf files without {Slow,VerySlow}" This reverts commit a9972c000bda4d8606fe572556d4256614e5f8f7. | 17 July 2021, 00:48:00 UTC |
refs/heads/PLDI-2020-perf-data | fdf45bb | Add perf data | 27 October 2019, 19:20:08 UTC |
refs/heads/POPL-2022-perf-data | c85e1c7 | Update perf txt/csv ``` time make COQBIN="$HOME/.local64/coq/coq-8.11.1/bin/" SKIP_BEDROCK2=1 TIMED=1 --output-sync perf-csv perf-txts ``` | 16 July 2021, 22:50:11 UTC |
refs/heads/PhD-Dissertation-2021-perf-data | fdf45bb | Add perf data | 27 October 2019, 19:20:08 UTC |
refs/heads/PhD-Dissertation-2021-perf-data-newer | 0160d22 | Add perf data From `make perf-Sanity perf-SuperFast perf-Fast perf-Medium; make perf-txts perf-csv perf-fits` | 16 January 2021, 22:35:51 UTC |
refs/heads/alpine-testing | c07f206 | Update coq-alpine.yml | 25 December 2023, 02:13:11 UTC |
refs/heads/master | 19f344b | speedup wf{3,4}_of_wf by factorizing raw matches to definitions (#157) This greatly reduces term size (tree size 1988106 -> 1121651 for wf3_of_wf). Timings before: (Succeed Qed includes some time which isn't in Time Qed, see also https://github.com/coq/coq/pull/19426) wf3 tactics 2.2s qed 1.09s succeed qed 1.25s wf4 tactics 14.5s qed 7.4s succeed qed 8.5s After: wf3 tactics 1.4s qed 0.6s succeed qed 0.65s wf4 tactics 8s qed 3.6s succeed qed 4s | 29 July 2024, 21:55:44 UTC |
refs/tags/v0.0.1 | ace6ea0 | Adapt to fixing dropped implicit arguments in Context. | 20 November 2020, 07:38:37 UTC |
refs/tags/v0.0.10 | a7f66c4 | Better describe-system-config | 24 December 2023, 01:05:20 UTC |
refs/tags/v0.0.11 | 21b82e9 | Adapt to coq/coq#18624 (Tac2ffi / Tac2val split) (#149) * Add separate files for v8.20 Everything except Makefile changes done with ``` for i in $(git ls-files "*.v819"); do cp $i ${i/v819/v820}; git add ${i/v819/v820}; done ``` * Adapt to coq/coq#18624 (Tac2ffi / Tac2val split) | 07 February 2024, 18:04:37 UTC |
refs/tags/v0.0.2 | 10c6a00 | Bump etc/coq-scripts from `3be05c7` to `7e68a28` (#39) | 17 March 2022, 22:03:44 UTC |
refs/tags/v0.0.3 | f18f187 | Bump etc/coq-scripts from `0ca86bb` to `d85c149` (#44) | 13 June 2022, 17:09:23 UTC |
refs/tags/v0.0.4 | a7e88a2 | Fix check-all run | 10 August 2022, 18:12:06 UTC |
refs/tags/v0.0.5 | 67901e0 | Merge pull request #62 from JasonGross/ltac2-reify-more Port rewrite rule reification to Ltac2 for improved performance | 02 October 2022, 11:43:59 UTC |
refs/tags/v0.0.6 | 6055c74 | Revert "Factor lift_existT into expr_to_pattern_and_replacement_unfolded{,_split} in reify_to_pattern_and_replacement_in_context" This reverts commit 499ea11a30f18a515e01f5603906f2b35b156be9. It seems to break fiat-crypto | 03 October 2022, 02:58:40 UTC |
refs/tags/v0.0.7 | 1d2dc36 | Add generated Ltac2Extra.v to .gitignore | 07 October 2022, 14:02:40 UTC |
refs/tags/v0.0.8 | 77c76a4 | adapt for coq/coq#17022 (#96) | 15 February 2023, 04:05:22 UTC |
refs/tags/v0.0.9 | 43447bc | `Proj.equal` has been upstreamed, so use it directly (#114) | 19 September 2023, 18:26:17 UTC |