Jason Gross
Jason Gross
It would be nice to be able to write something like `coqbot merge if CI passes` and have the bot wait until the CI passes and only merge if it...
#### Description of the problem Currently migrated bugs link to bugzilla attachments. [GitHub supports uploading `.txt`, `.log`, and `.zip` files](https://help.github.com/articles/file-attachments-on-issues-and-pull-requests/) as attachments on issues. I propose that for all bugs...
I'm reviewing coq/coq#12218, and seeing a lot of code that I believe will be wrong in the presence of casts, let-ins, and reducible matches (`if true then ... else ...`)...
Running ``` sudo apt-get update -y sudo apt-get install -y python3 python3-pip python3 -m pip install pyinstaller ``` works find on [Coq 8.4](https://github.com/JasonGross/coq-tools/actions/runs/6590449670/job/17921108906) and [Coq 8.6](https://github.com/JasonGross/coq-tools/actions/runs/6590449670/job/17921108541) but fails on [Coq...
Would it be possible to provide images for 8.8.dev, 8.9.dev, etc, tracking the tip of the v8.8, v8.9, etc branches? I'd like to use these for https://github.com/coq-community/coq-performance-tests after merging https://github.com/coq/coq/pull/16238,...
On https://docs.travis-ci.com/user/deployment-v2/providers/pages/#known-options , there is no default mentioned for `allow_empty_commit`, `verbose`, `committer_from_gh`, and others.  The v1 docs [here](https://docs.travis-ci.com/user/deployment/pages/#further-configuration) have defaults for many of these options: 
``` coq (* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from\ 351 lines to 260...
The following code works in coq 8.4, but not in HoTT/coq: ``` coq Set Implicit Arguments. Set Universe Polymorphism. Generalizable All Variables. Record SpecializedCategory (obj : Type) := { Object...
This code fails in HoTT/Coq, but does not if I remove the `change` (`present_obj`) or `intros` lines: ``` Coq Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. Polymorphic Record...
``` coq (* File reduced by coq-bug-finder from 520 lines to 9 lines. *) Set Universe Polymorphism. Class IsPointed (A : Type) := point : A. Generalizable Variables A B...