| 0ca86bb | Jason Gross | 26 March 2022, 01:15:40 UTC | clean all deletes timing log files :-( | 26 March 2022, 01:15:40 UTC |
| 34f450c | Jason Gross | 25 March 2022, 23:29:12 UTC | cleanall for diff timing | 25 March 2022, 23:29:12 UTC |
| 7e68a28 | Pierre Roux | 17 March 2022, 04:39:58 UTC | Adapt to https://github.com/coq/coq/pull/15754 (#9) | 17 March 2022, 04:39:58 UTC |
| 3be05c7 | Jason Gross | 16 December 2021, 02:15:59 UTC | Display unterminated errors by default on GH actions Because we wrap coqc in most instances of this script, it's fine to allow errors to be unterminated | 16 December 2021, 02:15:59 UTC |
| c34a5e9 | Jason Gross | 16 November 2021, 15:59:45 UTC | Merge pull request #8 from SkySkimmer/pre-816 Compatibility for Coq 8.16 | 16 November 2021, 15:59:45 UTC |
| e55edc0 | Gaëtan Gilbert | 16 November 2021, 13:21:11 UTC | Compatibility for Coq 8.16 Generated with ```bash export V=16; cp compatibility/Coq__master__Compat.v.in compatibility/Coq__8_${V}__Compat.v.in && sed "s/8_$(($V-1))/8_$(($V-1)) 8_$V/g" -i compatibility/generate-compat-files.sh && ./compatibility/generate-compat-files.sh && git add compatibility/Coq__8_${V}__Compat.v{,.in} ``` | 16 November 2021, 13:21:11 UTC |
| b66ed67 | Pierre Roux | 02 September 2021, 09:02:54 UTC | Adapt to coq/coq#14819 | 02 September 2021, 09:42:00 UTC |
| 97e207d | Jason Gross | 08 June 2021, 21:48:18 UTC | Regenerate compat files | 08 June 2021, 21:48:18 UTC |
| 442a8f6 | Jason Gross | 08 June 2021, 15:21:00 UTC | Make 8.14 compat file more future-proof Now it uses Coq.Compat.Coq814, so it'll be good for a couple more versions. | 08 June 2021, 15:21:00 UTC |
| 04ea182 | Jason Gross | 08 June 2021, 15:01:15 UTC | Compatibility for Coq 8.15 Generated with ```bash export V=15; cp compatibility/Coq__master__Compat.v.in compatibility/Coq__8_${V}__Compat.v.in && sed "s/8_$(($V-1))/8_$(($V-1)) 8_$V/g" -i compatibility/generate-compat-files.sh && ./compatibility/generate-compat-files.sh && git add compatibility/Coq__8_${V}__Compat.v{,.in} ``` | 08 June 2021, 15:01:15 UTC |
| 8483cc7 | Jason Gross | 08 June 2021, 14:57:06 UTC | Allow calling generate-compat-files.sh from any directory | 08 June 2021, 14:57:06 UTC |
| 1d6880c | Jason Gross | 03 May 2021, 15:35:19 UTC | Catch user errors that result in command exits | 03 May 2021, 15:35:19 UTC |
| 5890fbb | Jason Gross | 28 April 2021, 15:54:14 UTC | Fix some comments | 28 April 2021, 15:54:30 UTC |
| 1ad4075 | Jason Gross | 26 April 2021, 11:20:22 UTC | Add --stdout to support reading from stdout for GH Actions | 26 April 2021, 11:20:22 UTC |
| 9e57db9 | Jason Gross | 22 April 2021, 19:51:53 UTC | Add a fancier reportify script This script can now handle the full output of `make` and will do its best to detect when errors have terminated. We also behave better with regard to ensuring that we emit output once the parent process has finished. | 22 April 2021, 19:57:57 UTC |
| 2610bf6 | Jason Gross | 20 April 2021, 12:20:59 UTC | Allow pipe_stderr and reportify-coq to be nested | 20 April 2021, 12:20:59 UTC |
| e443917 | Jason Gross | 16 April 2021, 20:10:26 UTC | Fancier handling of warnings and errors | 16 April 2021, 20:10:26 UTC |
| 129e473 | Jason Gross | 16 April 2021, 18:17:33 UTC | Pass through messages to GH Actions unmolested | 16 April 2021, 18:17:33 UTC |
| 03d0ca4 | Jason Gross | 16 April 2021, 18:10:39 UTC | Fix severity handling | 16 April 2021, 18:10:39 UTC |
| d404f23 | Jason Gross | 16 April 2021, 18:07:14 UTC | Add scripts to directly report errors | 16 April 2021, 18:07:14 UTC |
| 84e5028 | Jason Gross | 16 April 2021, 17:11:43 UTC | Add pipe_stderr for use with the onelinify script | 16 April 2021, 17:11:43 UTC |
| 2fd96c9 | Jason Gross | 16 April 2021, 17:09:19 UTC | Revert "Adjust end of line on problem matcher" This reverts commit 03095fb71a58666fdeda8ecf1082d2ded6df710a. It's no longer needed now that we have a smarter onelinifier | 16 April 2021, 17:09:19 UTC |
| 43a44a1 | Jason Gross | 16 April 2021, 17:07:35 UTC | Better processing of errors Maybe we'll also be able to distinguish between warnings and errors if we want to. | 16 April 2021, 17:07:35 UTC |
| 03095fb | Jason Gross | 16 April 2021, 16:58:02 UTC | Adjust end of line on problem matcher There's an extra %0A at the end due to how the onelineifier works | 16 April 2021, 16:58:02 UTC |
| 2ab8e64 | Jason Gross | 16 April 2021, 16:43:10 UTC | Add a bunch of GH Actions problem matchers | 16 April 2021, 16:43:10 UTC |
| e84126c | Jason Gross | 16 April 2021, 16:37:57 UTC | Make a script for processing Coq errors for GH actions | 16 April 2021, 16:37:57 UTC |
| 37c5b72 | Jason Gross | 23 February 2021, 15:57:39 UTC | Update to num_int for compat with coq/coq#13842 | 23 February 2021, 15:57:39 UTC |
| 66f4089 | Jason Gross | 10 December 2020, 22:57:54 UTC | Update compat for https://github.com/coq/coq/pull/13559 | 10 December 2020, 22:57:54 UTC |
| dcc8719 | Jason Gross | 10 December 2020, 00:34:31 UTC | TEMP be more verbose in testing ml files for debugging CI | 10 December 2020, 00:34:31 UTC |
| 4cf888b | Jason Gross | 08 December 2020, 17:18:00 UTC | Disable native compiler | 08 December 2020, 17:18:00 UTC |
| 7a12f7a | Jason Gross | 08 December 2020, 01:38:29 UTC | Try again (coq got -native-compiler before it got -native-compiler no) | 08 December 2020, 01:38:29 UTC |
| 8987838 | Jason Gross | 08 December 2020, 01:21:02 UTC | Fix native-compiler support | 08 December 2020, 01:21:02 UTC |
| 2cd0774 | Jason Gross | 08 December 2020, 01:11:20 UTC | Add special support for -native-compiler ondemand To handle https://github.com/coq/coq/pull/13352 | 08 December 2020, 01:11:20 UTC |
| c14002c | Jason Gross | 24 November 2020, 18:50:56 UTC | Add compat for Coq 8.14 Generated by compatibility/bump-versions.sh | 24 November 2020, 18:50:56 UTC |
| 9464ceb | Jason Gross | 21 September 2020, 16:44:08 UTC | Make timing script robust against interleaving See also https://github.com/coq/coq/pull/13063 | 21 September 2020, 16:44:08 UTC |
| f8301bb | Jason Gross | 26 August 2020, 23:05:57 UTC | Drop r_syntax_plugin for compat with coq/coq#12218 Once https://github.com/coq/coq/pull/12218 is merged, we won't need r_syntax_plugin. But I don't think fiat ever used it anyway... | 26 August 2020, 23:06:51 UTC |
| d0b8e80 | Jason Gross | 23 May 2020, 23:07:48 UTC | Integrate https://github.com/coq/coq/pull/12388 | 23 May 2020, 23:07:48 UTC |
| bd89a4d | Jason Gross | 19 May 2020, 22:35:40 UTC | Port TimeFileMaker.py From https://github.com/coq/coq/pull/12368 | 19 May 2020, 22:35:40 UTC |
| 6481438 | Jason Gross | 18 May 2020, 19:10:35 UTC | Add compat for 8.13 Generated by compatibility/bump-versions.sh | 18 May 2020, 19:10:35 UTC |
| 80dfb92 | Jason Gross | 18 May 2020, 19:10:17 UTC | Add compatibility/bump-versions.sh | 18 May 2020, 19:10:17 UTC |
| 6512d7a | Jason Gross | 18 May 2020, 19:00:51 UTC | Don't require updates to the Makefile on every version bump | 18 May 2020, 19:00:51 UTC |
| a1a302d | Jason Gross | 18 April 2020, 21:52:49 UTC | Add memory-based sorting Copied from https://github.com/coq/coq/pull/11606 | 18 April 2020, 21:52:49 UTC |
| d2b185c | Jason Gross | 08 April 2020, 04:39:19 UTC | Fix a missing || echo Error in the previous commit | 08 April 2020, 04:39:19 UTC |
| 5e20170 | Jason Gross | 08 April 2020, 04:10:54 UTC | Add support for -require-import See https://github.com/coq/coq/pull/12005#issuecomment-608274472 | 08 April 2020, 04:10:54 UTC |
| e26c8db | Jason Gross | 17 March 2020, 02:10:10 UTC | Fix insert-timings.sh for coqc -time | 17 March 2020, 02:10:10 UTC |
| 371f583 | Jason Gross | 26 February 2020, 04:12:09 UTC | Right-align rather than left-align Tables look better this way | 26 February 2020, 04:12:09 UTC |
| 4d90739 | Jason Gross | 16 February 2020, 02:02:24 UTC | Use --output-sync, and be robust to non-sync logs We now don't error if time keys are not present | 16 February 2020, 02:02:24 UTC |
| 2391f3a | Jason Gross | 14 February 2020, 22:32:01 UTC | Updated timing scripts with the latest versions from Coq itself C.f. https://github.com/coq/coq/pull/11606 | 14 February 2020, 22:32:45 UTC |
| b4a8fb0 | Jason Gross | 06 February 2020, 00:27:25 UTC | Update make-pretty-timed-only-diff-tip.sh Add auto-hiding in the usage comment | 06 February 2020, 00:27:25 UTC |
| ee398eb | Jason Gross | 06 February 2020, 00:26:41 UTC | Update make-pretty-timed-diff-tip.sh Have auto-hiding in the comment | 06 February 2020, 00:26:41 UTC |
| c9ae997 | Jason Gross | 31 January 2020, 03:53:36 UTC | Support submodule changes across commits | 31 January 2020, 03:53:36 UTC |
| 3dd416c | Jason Gross | 26 November 2019, 18:52:22 UTC | Don't run coq_makefile twice in parallel; get rid of the .conf target | 26 November 2019, 18:52:22 UTC |
| 3fc7abc | Jason Gross | 25 November 2019, 04:22:32 UTC | Allow setting INSTALLDEFAULTROOT | 25 November 2019, 04:22:32 UTC |
| f646fb5 | Jason Gross | 25 November 2019, 02:17:48 UTC | Remove primints from compat They were not available in 8.9 And fiat doesn't use them anyway | 25 November 2019, 02:17:48 UTC |
| b7d67c8 | Jason Gross | 24 November 2019, 23:04:30 UTC | Add support for Coq v8.12 (untested) | 24 November 2019, 23:04:30 UTC |
| d306f55 | Jason Gross | 02 November 2019, 22:29:21 UTC | Update compat stuff to work with coq/coq#11032 | 02 November 2019, 22:29:21 UTC |
| ae808ae | Jason Gross | 01 November 2019, 16:53:36 UTC | Update vo_closure to work after coq/coq#10947 Closes coq/coq#11023 | 01 November 2019, 16:53:36 UTC |
| db0ebbd | Jason Gross | 16 October 2019, 02:05:36 UTC | Allow ocaml compat to work even if we don't include Makefile.coq.common | 16 October 2019, 02:06:14 UTC |
| 6bcc15b | Jason Gross | 22 August 2019, 07:00:38 UTC | Switch from python2 to python3 Closes #6 | 22 August 2019, 07:00:38 UTC |
| 018efd2 | Jason Gross | 17 April 2019, 19:24:20 UTC | Preliminary support for 8.11 | 17 April 2019, 19:24:20 UTC |
| 9dc70c7 | Jason Gross | 11 March 2019, 21:34:22 UTC | Merge pull request #5 from cpitclaudel/master Change VectorDef to Vector to work around OCaml extraction issues | 11 March 2019, 21:34:22 UTC |
| a23081e | Clément Pit-Claudel | 01 February 2019, 14:11:39 UTC | Change VectorDef to Vector to work around OCaml extraction issues Closes #4. | 01 February 2019, 14:11:39 UTC |
| 2187c33 | Jason Gross | 08 January 2019, 19:46:04 UTC | Be a bit more verbose to catch more errors This should prevent issues like https://github.com/mit-plv/fiat/pull/21 in the future, hopefully. | 08 January 2019, 19:46:04 UTC |
| 7b0f426 | Jason Gross | 10 November 2018, 02:39:22 UTC | Fix a typo | 10 November 2018, 02:39:22 UTC |
| 386ba0d | Jason Gross | 10 November 2018, 02:28:10 UTC | Add support for sed in changing _CoqProject.in to _CoqProject | 10 November 2018, 02:28:10 UTC |
| 462dde5 | Jason Gross | 11 September 2018, 18:34:10 UTC | Add support for Coq 8.10 | 11 September 2018, 18:36:18 UTC |
| 716247b | Jason Gross | 02 September 2018, 19:29:18 UTC | Update clean target | 02 September 2018, 19:29:18 UTC |
| 71d5a15 | Jason Gross | 24 August 2018, 00:10:20 UTC | Grab Coq.Compat.Coq88 for new versions of Coq This allows us to be compatible with the new behavior of prim token syntax (https://github.com/coq/coq/pull/8064 and https://github.com/coq/coq/pull/8064#issuecomment-415493362) without having to export unqualified String names everywhere. | 24 August 2018, 00:10:20 UTC |
| 7aa4366 | Jason Gross | 07 June 2018, 23:49:49 UTC | Add support for 8.9 | 07 June 2018, 23:50:03 UTC |
| ef2d7f9 | Jason Gross | 15 April 2018, 21:43:08 UTC | Revert "Use a faster method for reading deps from a single file" This reverts commit 5dc2bd6dca55c89d9305672252ab4380e5a9550b. It is a buggy way of doing things. Maybe this should be moved to python... | 15 April 2018, 21:43:08 UTC |
| 5dc2bd6 | Jason Gross | 15 April 2018, 18:53:32 UTC | Use a faster method for reading deps from a single file | 15 April 2018, 18:53:32 UTC |
| 7bd683d | Jason Gross | 27 December 2017, 01:06:00 UTC | Handle VDFILE in makefile compat | 27 December 2017, 01:06:00 UTC |
| b8e11b4 | Jason Gross | 08 December 2017, 16:09:59 UTC | Support Coq 8.8 in vo_closure If VDFILE is defined, we assume coqdep puts all dependencies in `$(VDFILE).d`, as per https://github.com/coq/coq/pull/6217. | 08 December 2017, 16:09:59 UTC |
| ca779ea | Jason Gross | 08 December 2017, 15:52:30 UTC | Prep for the day when we have only a single .v.d file | 08 December 2017, 15:52:30 UTC |
| 617ccff | Jason Gross | 13 November 2017, 18:55:38 UTC | Fix sorting order on timing diff | 13 November 2017, 18:55:38 UTC |
| 14a82bf | Jason Gross | 31 October 2017, 22:06:52 UTC | Update timing python scripts Integrate changes added when merging into Coq | 31 October 2017, 22:06:52 UTC |
| f800570 | Jason Gross | 06 October 2017, 06:52:34 UTC | Permit trailing whitespace This makes it work better with logs from travis | 06 October 2017, 06:52:34 UTC |
| 25e7262 | Jason Gross | 02 September 2017, 14:48:35 UTC | Add v8.8 compat | 02 September 2017, 14:48:35 UTC |
| 8d897df | Jason Gross | 11 August 2017, 17:14:46 UTC | Mention PREV_COMMIT in docs of pretty-timed-*diff-tip.sh files | 11 August 2017, 17:14:46 UTC |
| ca4ba88 | Jason Gross | 06 July 2017, 23:05:50 UTC | Handle detached head state in *tip*.sh This should close #3 (untested) | 06 July 2017, 23:05:50 UTC |
| 3dc1a8f | Jason Gross | 06 July 2017, 21:52:18 UTC | Add support for master, v8.7 | 06 July 2017, 21:52:18 UTC |
| 4c041ea | Jason Gross | 29 June 2017, 03:05:47 UTC | Better support for Windows in timing | 29 June 2017, 03:05:47 UTC |
| 258ae46 | Jason Gross | 28 June 2017, 05:43:05 UTC | Fix quoting problem of OCAMLFIND on Windows | 28 June 2017, 05:43:05 UTC |
| d9be488 | Jason Gross | 15 June 2017, 20:34:31 UTC | Update trunk compat file for funind change | 15 June 2017, 20:34:31 UTC |
| ef47bc0 | Jason Gross | 15 June 2017, 16:15:53 UTC | Fix -compat 8.4 check Look for "Error", since trunk says "Error: Compatibility with version ..." | 15 June 2017, 16:15:53 UTC |
| 3203b97 | Jason Gross | 12 June 2017, 16:03:00 UTC | Proper support for -bypass-API | 12 June 2017, 16:03:00 UTC |
| ced5c13 | Jason Gross | 08 June 2017, 17:09:23 UTC | Add partial support for -bypass-API (not sure if it's needed) | 08 June 2017, 17:09:23 UTC |
| aab93f9 | Jason Gross | 06 June 2017, 18:08:53 UTC | Add make-pretty-timed-or-error.sh | 06 June 2017, 18:08:53 UTC |
| d757382 | Jason Gross | 11 May 2017, 00:06:04 UTC | Re-support 8.4, 8.5 in test-exists-ml-function Apparently outputting a coq Makefile in a different directory only started working in Coq 8.6. | 11 May 2017, 00:06:54 UTC |
| 6836b4a | Jason Gross | 10 May 2017, 23:58:12 UTC | Also cleanup coq_makefile2 conf file | 10 May 2017, 23:58:12 UTC |
| 382a6a1 | Jason Gross | 10 May 2017, 22:28:22 UTC | Actually make use of sed commands I made a mistake when adding a use of -o to coq_makefile | 10 May 2017, 22:28:22 UTC |
| df21afb | Jason Gross | 10 May 2017, 20:56:56 UTC | Create README.md in timing folder | 10 May 2017, 20:56:56 UTC |
| c47289a | Jason Gross | 10 May 2017, 20:56:19 UTC | Improve doc of make-pretty-timed-only-diff.sh | 10 May 2017, 20:56:19 UTC |
| 5d0be40 | Jason Gross | 29 April 2017, 16:37:34 UTC | Use -o Makefile.coq.old This way, coq_makefile2 won't regenerate Makefile.coq without the sed commands | 29 April 2017, 16:37:34 UTC |
| 407e64d | Jason Gross | 29 April 2017, 16:27:13 UTC | Make warn-compat-file an order-only dependency We don't want to remake the compat file all the time, just because warn-compat-file is PHONY | 29 April 2017, 16:27:13 UTC |
| 8df9fd1 | Jason Gross | 29 April 2017, 02:07:05 UTC | Use -o in coq_makefile | 29 April 2017, 02:07:05 UTC |
| c905e81 | Jason Gross | 29 April 2017, 02:03:52 UTC | Use a temporary file for conftest | 29 April 2017, 02:04:18 UTC |
| 3ff5974 | Jason Gross | 29 April 2017, 02:03:35 UTC | Only disable inclusion of .d files | 29 April 2017, 02:04:18 UTC |
| 878fffa | Jason Gross | 09 April 2017, 16:16:44 UTC | Preserve first arguent to vo_reverse_closure | 09 April 2017, 16:16:44 UTC |
| 5c40045 | Jason Gross | 09 April 2017, 16:14:50 UTC | Add vo_reverse_closure | 09 April 2017, 16:14:50 UTC |
