| 26f9768 | Jason Gross | 09 April 2022, 12:33:46 UTC | Add MacOS CI | 09 April 2022, 12:33:46 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 |
| 04dc1ae | Jason Gross | 03 July 2021, 00:06:44 UTC | Fix circular import | 03 July 2021, 00:07:02 UTC |
| 6731ede | Jason Gross | 02 July 2021, 23:47:41 UTC | Pass -d native-compiler when it's allowed This makes things less needlessly verbose | 02 July 2021, 23:47:41 UTC |
| 955e9c6 | Jason Gross | 02 July 2021, 22:29:24 UTC | Fix debug retry on native mismatch Also remove long-dead comment and now-useless verbose debug output | 02 July 2021, 22:29:24 UTC |
| 3bc0aab | Jason Gross | 02 July 2021, 22:18:24 UTC | More verbose debugging | 02 July 2021, 22:18:24 UTC |
| 803f67e | Jason Gross | 02 July 2021, 21:51:49 UTC | Add more verbose debug output | 02 July 2021, 21:51:49 UTC |
| e2335ac | Jason Gross | 02 July 2021, 18:34:01 UTC | Pass -debug to coqc when native compute has an interface mismatch Hopefully this will help us debug things by keeping the temporary files around | 02 July 2021, 18:34:01 UTC |
| 881760f | Jason Gross | 02 July 2021, 14:14:23 UTC | Fix for Coq <= 8.5 | 02 July 2021, 14:14:23 UTC |
| e3f34c9 | Jason Gross | 02 July 2021, 06:42:10 UTC | MANGLED => WRAPPED ``` git grep --name-only MANGLED | xargs sed -i 's/MANGLED/WRAPPED/g' ``` | 02 July 2021, 06:42:10 UTC |
| 74f06c5 | Jason Gross | 02 July 2021, 02:03:28 UTC | Use an alternate strategy for inlining We base things on `Include` instead. Not as good as if we had https://github.com/coq/coq/issues/14541, but still fixes #67, as per https://github.com/JasonGross/coq-tools/issues/67#issuecomment-872639302 | 02 July 2021, 02:05:08 UTC |
