a47ed37 | Jason Gross | 12 July 2022, 18:21:59 UTC | Remove path sensitivity in traceback output, test 12 | 12 July 2022, 18:21:59 UTC |
d99f778 | Jason Gross | 29 June 2022, 01:58:36 UTC | Also augment passing_coqtop_args with paths This should fix some issues that cropped up in https://github.com/coq/coq/pull/16190, oops | 29 June 2022, 01:58:36 UTC |
0528f1b | Jason Gross | 24 June 2022, 19:58:38 UTC | Split statements to definitions with passing coqc (#126) Should deal with https://github.com/coq/coq/pull/16190#issuecomment-1164689959 | 24 June 2022, 19:58:38 UTC |
e3441e3 | Jason Gross | 24 June 2022, 13:33:42 UTC | Add a CI job to check previous step success This will let us mandate that all steps pass on CI for PRs without having to list them out exhaustively. | 24 June 2022, 13:35:19 UTC |
0aa7b72 | Jason Gross | 24 June 2022, 13:23:09 UTC | Use default ocaml version in ci-dev (#125) Fixes #124 | 24 June 2022, 13:23:09 UTC |
2db278b | Jason Gross | 22 June 2022, 20:47:15 UTC | Be more lax in universe matching in some error messages Should allow us to minimize https://github.com/coq/coq/pull/16190#issuecomment-1162320146 | 22 June 2022, 20:47:46 UTC |
fe297b1 | Jason Gross | 21 June 2022, 01:41:54 UTC | Add new versions of Coq to CI (#119) | 21 June 2022, 01:41:54 UTC |
dcfab4a | dependabot[bot] | 09 June 2022, 01:34:22 UTC | Bump actions/setup-python from 3 to 4 (#120) | 09 June 2022, 01:34:22 UTC |
e16e6b5 | Jason Gross | 04 June 2022, 02:27:28 UTC | Add 8.14, 8.15, and switch dev to 4.13+flambda c.f. 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 | 04 June 2022, 02:27:28 UTC |
dbe8db0 | Jason Gross | 09 April 2022, 14:56:57 UTC | Pass `KEEP_ERROR=1` unless coq_makefile is old (#117) Should deal with the bug exposed by https://github.com/coq/coq/pull/15880 | 09 April 2022, 14:56:57 UTC |
4069e6b | Jason Gross | 09 April 2022, 11:51:16 UTC | Use `/usr/bin/env bash` As per https://github.com/JasonGross/coq-tools/issues/118 | 09 April 2022, 11:51:16 UTC |
9ee0828 | dependabot[bot] | 02 March 2022, 01:39:23 UTC | Bump actions/checkout from 2 to 3 (#116) | 02 March 2022, 01:39:23 UTC |
faf126b | dependabot[bot] | 01 March 2022, 02:07:50 UTC | Bump actions/setup-python from 2.3.2 to 3 (#115) | 01 March 2022, 02:07:50 UTC |
282c529 | Ali Caglayan | 14 February 2022, 03:17:33 UTC | add color for success/nothing changed messages (#114) * add color for success/nothing changed messages * use better escape character * added --no-color option and refactored color code * change coloron -> color_on * Better help for --no-color | 14 February 2022, 03:17:33 UTC |
ecc16a5 | Jason Gross | 11 February 2022, 06:05:36 UTC | Log a bit more info to deal with confusing grouping of goals | 11 February 2022, 06:05:36 UTC |
abedb0e | Jason Gross | 10 February 2022, 17:14:52 UTC | `Fail foo` succeeding is not an error Should resolve https://github.com/coq/coq/pull/14748#issuecomment-1034554482 / https://github.com/coq/coq/pull/15653#issuecomment-1034134695 | 10 February 2022, 17:14:52 UTC |
60b508a | Jason Gross | 10 February 2022, 06:14:50 UTC | Only write to the temp file on init or inlining failures Fixes #106 and #103 (I hope) | 10 February 2022, 06:14:50 UTC |
ccc00c5 | Jason Gross | 07 February 2022, 21:50:50 UTC | More flexible anomaly detection in a particular case Fixes #111 (hopefully) | 07 February 2022, 21:50:50 UTC |
6d81ec0 | Jason Gross | 07 February 2022, 21:24:02 UTC | Reset the timeout when trying multiple inliners Fixes #110 | 07 February 2022, 21:24:02 UTC |
fd38a2f | dependabot[bot] | 07 February 2022, 02:17:18 UTC | Bump actions/setup-python from 2.3.1 to 2.3.2 (#109) | 07 February 2022, 02:17:18 UTC |
6ce8691 | Jason Gross | 17 January 2022, 19:43:08 UTC | Be more robust in absolutizing files (#104) Works around https://github.com/coq/coq/issues/15497, fixing bedrock2 issue that arose at https://github.com/coq/coq/pull/15487#issuecomment-1013700274 | 17 January 2022, 19:43:08 UTC |
83a8d7a | Jason Gross | 17 January 2022, 18:20:14 UTC | Add a bit more logging | 17 January 2022, 18:20:14 UTC |
3ee2e3e | Enrico Tassi | 16 December 2021, 17:04:25 UTC | Update coq_running_support.py Co-authored-by: Jason Gross <jasongross9@gmail.com> | 16 December 2021, 19:26:30 UTC |
68372cd | Enrico Tassi | 09 December 2021, 09:03:01 UTC | adapt to coq/coq#15220 | 16 December 2021, 19:26:30 UTC |
f270f5a | dependabot[bot] | 30 November 2021, 00:36:34 UTC | Merge pull request #99 from JasonGross/dependabot/github_actions/actions/setup-python-2.3.1 | 30 November 2021, 00:36:34 UTC |
586cef7 | dependabot[bot] | 29 November 2021, 18:29:49 UTC | Bump actions/setup-python from 1 to 2.3.1 Bumps [actions/setup-python](https://github.com/actions/setup-python) from 1 to 2.3.1. - [Release notes](https://github.com/actions/setup-python/releases) - [Commits](https://github.com/actions/setup-python/compare/v1...v2.3.1) --- updated-dependencies: - dependency-name: actions/setup-python dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <support@github.com> | 29 November 2021, 18:29:49 UTC |
486d362 | Jason Gross | 29 November 2021, 18:29:22 UTC | Create dependabot.yml | 29 November 2021, 18:29:22 UTC |
d87641a | Jason Gross | 17 November 2021, 20:08:56 UTC | More robust native compiler warning silencing | 18 November 2021, 01:24:47 UTC |
5738768 | Jason Gross | 14 November 2021, 23:44:12 UTC | Move dev branches to docker action This will hopefully make them more easily restartable when master changes | 18 November 2021, 01:24:47 UTC |
e7364d4 | Jason Gross | 18 November 2021, 01:23:24 UTC | Try one more combination when inlining modules It might be the case that we need requires right where they are, and can't insert them at the top | 18 November 2021, 01:23:24 UTC |
b2faa75 | Jason Gross | 17 November 2021, 16:10:54 UTC | Test 49 does not work on Coq 8.4 due to lack of topname support in minimizer We could make it work, but we'd have to start piping through topname separately from the arguments to Coq. We should probably do this anyway at some point. | 18 November 2021, 00:10:18 UTC |
14a00d0 | Jason Gross | 17 November 2021, 16:04:48 UTC | Fix example 00 for 8.4 8.4 does not support the -top argument, so the way we're piping the topname does not work | 18 November 2021, 00:10:18 UTC |
3bc853c | Jason Gross | 14 November 2021, 23:44:12 UTC | Add a docker action to test 8.4 | 18 November 2021, 00:10:18 UTC |
47b3fb3 | Jason Gross | 15 November 2021, 17:22:22 UTC | Fix for coqtop but not coqc accepts top | 18 November 2021, 00:10:18 UTC |
07bb27e | Jason Gross | 15 November 2021, 17:13:02 UTC | Also handle -topfile in coqtop-as-coqc | 18 November 2021, 00:10:18 UTC |
e718257 | Jason Gross | 15 November 2021, 16:46:02 UTC | Arrange argument ordering for 8.4 compat | 18 November 2021, 00:10:18 UTC |
3d129cb | Jason Gross | 15 November 2021, 16:24:40 UTC | Use -nois rather than -noinit, for 8.4 compat | 18 November 2021, 00:10:18 UTC |
a35f036 | Jason Gross | 15 November 2021, 16:24:11 UTC | Fix 8.4 word wrapping and character location changes | 18 November 2021, 00:10:18 UTC |
eff50e8 | Jason Gross | 15 November 2021, 16:16:59 UTC | 8.4 does not support -Q | 18 November 2021, 00:10:18 UTC |
0c4e465 | Jason Gross | 15 November 2021, 16:13:49 UTC | Replace Lia with a module present in both 8.4 and later | 18 November 2021, 00:10:18 UTC |
df16692 | Jason Gross | 17 November 2021, 20:21:27 UTC | Fix ex 46 for master | 17 November 2021, 23:03:42 UTC |
2fde508 | Jason Gross | 17 November 2021, 19:05:01 UTC | Smaller example 13 test | 17 November 2021, 23:03:42 UTC |
30d3323 | Jason Gross | 17 November 2021, 15:57:57 UTC | Fix example 13 for Coq 8.6(?) Not sure what's up here | 17 November 2021, 23:03:42 UTC |
2cf2c80 | Jason Gross | 16 November 2021, 03:18:45 UTC | Add proof mode setting for Ltac, so we can make use of splitting | 17 November 2021, 23:03:42 UTC |
c345fca | Jason Gross | 15 November 2021, 19:54:43 UTC | Fix defined_reg for Coq 8.4 | 17 November 2021, 23:03:42 UTC |
51040a7 | Jason Gross | 15 November 2021, 18:47:08 UTC | Fix definition splitting in Coq > 8.4 The location of timing messages changed, so we need to use a different strategy to find them. Also, we now actually check for the defined constants. | 17 November 2021, 23:03:42 UTC |
99b0b3d | Jason Gross | 15 November 2021, 01:24:32 UTC | Fix for exist_ok not on python 2.7 | 16 November 2021, 02:52:45 UTC |
b08c401 | Jason Gross | 14 November 2021, 23:48:36 UTC | Fix syntax error E999 SyntaxError: only named arguments may follow *expression | 16 November 2021, 02:52:45 UTC |
7151a02 | Jason Gross | 14 November 2021, 20:00:59 UTC | Since coqc doesn't respect -topname, we build the directory tree Fixes #91, mostly. (The making of glob files and absolutizing requires that occur after any dependency on topname is still going to fail :-/ ) | 16 November 2021, 02:52:45 UTC |
cf4e5db | Jason Gross | 15 November 2021, 17:42:43 UTC | Delete .vo and not just .glob | 15 November 2021, 17:42:43 UTC |
f8d9fe4 | Jason Gross | 15 November 2021, 17:37:13 UTC | More robust removal of .glob and .vo files | 15 November 2021, 17:37:13 UTC |
e7522dc | Jason Gross | 15 November 2021, 17:30:53 UTC | Better recursive deleting of .vo and .glob files | 15 November 2021, 17:30:53 UTC |
20ab53c | Jason Gross | 15 November 2021, 17:03:58 UTC | Fix From Require tests 32, 33 | 15 November 2021, 17:26:32 UTC |
cc814ee | Jason Gross | 15 November 2021, 16:54:49 UTC | Better handling of disabled tests | 15 November 2021, 16:55:47 UTC |
19b9b3e | Jason Gross | 15 November 2021, 16:55:34 UTC | Check for -w support | 15 November 2021, 16:55:34 UTC |
45be05e | Jason Gross | 14 November 2021, 19:12:36 UTC | Remove dead code | 14 November 2021, 23:49:15 UTC |
e9b5f87 | Jason Gross | 14 November 2021, 19:10:00 UTC | Move some functions around so diagnose_error can use group_coq_args | 14 November 2021, 23:49:15 UTC |
c7a68c1 | Jason Gross | 14 November 2021, 22:45:13 UTC | Rename coq-bug-finder to coq-bug-minimizer We may rename the python script at some point, too | 14 November 2021, 22:45:13 UTC |
1393a34 | Jason Gross | 12 November 2021, 20:33:13 UTC | _CoqProject files also list ocaml files | 12 November 2021, 20:33:20 UTC |
00f4652 | Jason Gross | 10 November 2021, 00:41:55 UTC | Make example_08-3 always run Now we have a workaround for coqtop not supporting -compile, which is using coqc instead for make. | 11 November 2021, 22:04:55 UTC |
1573370 | Jason Gross | 10 November 2021, 18:54:44 UTC | Fix test for coqtop -compile Coq 8.10 accepted -compile but raised an anomaly. | 11 November 2021, 22:04:55 UTC |
056335e | Jason Gross | 09 November 2021, 03:45:02 UTC | Add a pass that splits `Require` This will probably handle 99% of #78. What remains is a pass to move `Require` up as high as possible. | 10 November 2021, 18:57:03 UTC |
e8e8745 | Jason Gross | 09 November 2021, 22:50:19 UTC | Fix for making globs when coqc is coqtop Previously handled only in fill_kwargs in replace_imports | 10 November 2021, 18:45:46 UTC |
c500e2f | Jason Gross | 09 November 2021, 21:58:58 UTC | Fix newlines on older versions of Coq | 10 November 2021, 18:45:46 UTC |
db0bb99 | Jason Gross | 09 November 2021, 01:47:41 UTC | Run `normalize_requires` inside `minimize_file` This is partial progress on #78. What remains is a pass to split off `Require` from `Import`, and a pass to work on moving up `Require`s one at a time. | 10 November 2021, 18:45:46 UTC |
4baaaf8 | Jason Gross | 10 November 2021, 00:17:21 UTC | Quiety debug log when running with coqtop as coqc | 10 November 2021, 00:17:29 UTC |
4dbe57a | Jason Gross | 08 November 2021, 22:14:15 UTC | A bit more factoring | 09 November 2021, 03:47:48 UTC |
4faa038 | Jason Gross | 08 November 2021, 21:02:16 UTC | Split up update_with_glob | 09 November 2021, 03:47:48 UTC |
0dd460a | Jason Gross | 08 November 2021, 21:44:12 UTC | Fix classification of require export | 09 November 2021, 03:47:48 UTC |
86413a2 | Jason Gross | 08 November 2021, 19:52:32 UTC | Factor some use of glob files This changes the numbers in get_require_locations by 1, but I think that function was previously unused. | 09 November 2021, 03:47:48 UTC |
c04f0b3 | Jason Gross | 09 November 2021, 01:48:19 UTC | Minor simplification | 09 November 2021, 02:29:16 UTC |
c29c39c | Jason Gross | 05 November 2021, 01:22:54 UTC | Don't assume that _ is escaped | 05 November 2021, 01:22:54 UTC |
af9fbb2 | Jason Gross | 04 November 2021, 22:13:14 UTC | Allow filename replacements to be dotted libnames | 04 November 2021, 22:13:14 UTC |
69f5f6a | Jason Gross | 04 November 2021, 15:42:59 UTC | Display fatal messages in all logs This makes "The computed error message was not present in the given error log." show up on ci minimization reports. | 04 November 2021, 15:42:59 UTC |
116f50f | Jason Gross | 04 November 2021, 15:33:59 UTC | Don't depend on file name for error message Fixes failed minimization of https://github.com/coq/coq/pull/14746#issuecomment-960971850 | 04 November 2021, 15:33:59 UTC |
562f48c | Jason Gross | 03 November 2021, 16:33:24 UTC | Fix for python2.7 | 03 November 2021, 17:11:11 UTC |
f859a54 | Jason Gross | 03 November 2021, 15:50:59 UTC | Prefer `Admitted` rather than `admit. Defined` Fixes #79 I expect that admitting definitions does not take that much time (I believe most of the time is spent trying to remove each line one at a time), so we just try both. | 03 November 2021, 17:11:11 UTC |
9b39898 | Jason Gross | 27 October 2021, 19:26:59 UTC | Logging: different verbosities for different files Fixes #76 We invert the control-flow of verbosity logic and add `--verbose-log-file` (e.g., `--verbose-log-file 10,very-verbose.log 0,quiet.log 2,-`) to allow logging of different verbosities to different files. This will allow more verbose logging on CI minimization without polluting the displayed log. | 27 October 2021, 21:09:11 UTC |
c0fab71 | Jason Gross | 27 October 2021, 15:15:28 UTC | Fix timeout setting messages | 27 October 2021, 15:15:28 UTC |
9e1d862 | Jason Gross | 27 October 2021, 01:54:26 UTC | Fix a typo | 27 October 2021, 01:54:26 UTC |
764c867 | Jason Gross | 27 October 2021, 01:42:26 UTC | Fix error about multiple values of coqc | 27 October 2021, 01:42:26 UTC |
99d7a6e | Jason Gross | 27 October 2021, 01:25:42 UTC | Allow different timeouts for coqc and passing coqc This was breaking a bunch of things at https://github.com/coq/coq/pull/14748 The passing coqc is generally expected to take longer than the failing one, because it does more. | 27 October 2021, 01:28:04 UTC |
ed441c2 | Jason Gross | 27 October 2021, 00:10:49 UTC | Passing coqc timeout should not be considered success Oops. Should deal with https://github.com/coq/coq/pull/14746#issuecomment-894317692 | 27 October 2021, 00:13:03 UTC |
4b98560 | Jason Gross | 26 October 2021, 21:32:01 UTC | Disable test 48 on old Coq We need `Require Import Coq.Init.Ltac.` to work. I didn't want to bother trying to figure out how to support multiple Ltac support snippets in this very specific test. | 26 October 2021, 22:15:03 UTC |
d480fc4 | Jason Gross | 26 October 2021, 21:24:22 UTC | Force `False` axiom in `Prop` Fixes #74 This will handle https://github.com/coq/coq/pull/14733#issuecomment-892772832 and https://github.com/coq/coq/pull/14748#issuecomment-898896082 | 26 October 2021, 22:15:03 UTC |
719a2fe | Jason Gross | 19 October 2021, 20:04:50 UTC | Fix issue with example 8 | 19 October 2021, 20:04:50 UTC |
4d15b21 | Jason Gross | 19 October 2021, 18:51:24 UTC | Add metadata tracking the approximate build time Of generated files | 19 October 2021, 18:51:24 UTC |
d721738 | Jason Gross | 19 October 2021, 18:16:46 UTC | Add metadata about modules that failed to inline | 19 October 2021, 18:16:46 UTC |
71d4597 | Jason Gross | 19 October 2021, 17:36:22 UTC | Skip comments in _CoqProject Fixes #70 Reference: https://github.com/coq/coq/blob/79fff2993afb0ef553b1efe5612448b1d5e285c3/lib/coqProject_file.ml#L82-L116 | 19 October 2021, 17:36:22 UTC |
a0c173e | Jason Gross | 09 October 2021, 00:01:05 UTC | If inlining files, adjust imports as necessary Fixes #16, also deals with the issue at https://github.com/coq/coq/pull/14986#issuecomment-938600824 | 09 October 2021, 01:36:49 UTC |
d91a8c6 | Jason Gross | 03 August 2021, 16:15:07 UTC | Don't print fancy backtraces for EOFError This fixes the example that broke in a recent commit | 03 August 2021, 16:15:07 UTC |
97a6d9e | Jason Gross | 03 August 2021, 16:12:55 UTC | Revert "Factor out exception formatting a bit" This reverts commit 234bc2b7c3ba33112f107d7da003600b148bd008. | 03 August 2021, 16:12:55 UTC |
234bc2b | Jason Gross | 03 August 2021, 15:46:46 UTC | Factor out exception formatting a bit Factoring out the exception-formatting is my (perhaps-misguided) attempt to be extra-careful to not capture the wrong exception, and to be clear about printing the same exception in all versions. | 03 August 2021, 16:12:48 UTC |
b7f2ef6 | Jason Gross | 02 August 2021, 18:38:49 UTC | Better traceback reporting in new enough versions of python | 02 August 2021, 18:38:49 UTC |
fdcc5fb | Jason Gross | 06 July 2021, 19:11:42 UTC | Don't try to strip module( type)s with arguments We want to be able to strip empty sections even when line-by-line stripping doesn't work; stripping module types with arguments when line-by-line stripping is less important, because they're less common. | 06 July 2021, 19:11:44 UTC |
7c1dd19 | Jason Gross | 06 July 2021, 17:51:21 UTC | Don't pass -o on old versions of Coq that don't support it | 06 July 2021, 17:51:21 UTC |
f1aedb3 | Jason Gross | 06 July 2021, 17:39:34 UTC | Don't use make to make single glob files whose .vo already exists This allows us to dump the glob in the right location while dumping the .vo file in `/tmp`, so as to not clobber existing .vo files. This should resolve issues such as https://github.com/coq/coq/pull/14598#issuecomment-874009361 where ci-compcert fails to minimize because it generates .glob files in strange locations. | 06 July 2021, 17:44:16 UTC |
c78cd90 | Jason Gross | 03 July 2021, 02:07:43 UTC | Revert "TEMP Print more debug info for Coq minimization" This reverts commit 2dd2c21dd736807aa14600e9d8eb225f503046ee. | 03 July 2021, 02:07:43 UTC |
2dd2c21 | Jason Gross | 03 July 2021, 01:47:08 UTC | TEMP Print more debug info for Coq minimization | 03 July 2021, 01:47:08 UTC |
e4faaaa | Jason Gross | 03 July 2021, 00:53:48 UTC | More robust check for debug flag | 03 July 2021, 00:53:48 UTC |