Jason Gross

Results 540 issues of Jason Gross

``` $ make ghc --make -o tc Main.hs -fwarn-incomplete-patterns -Werror TypeChecker.hs:1:55: error: [-Werror] -XOverlappingInstances is deprecated: instead use per-instance pragmas OVERLAPPING/OVERLAPPABLE/OVERLAPS | 1 | {-# LANGUAGE UndecidableInstances, FlexibleInstances, OverlappingInstances #-}...

For future reference: we want to edit https://github.com/coq/bot/blob/master/bot-components/GitHub_mutations.ml and https://github.com/coq/bot/blob/master/bot-components/GitHub_GraphQL.ml and the references are: - https://docs.github.com/en/graphql/reference/mutations#addreaction - https://docs.github.com/en/graphql/reference/input-objects#addreactioninput - https://docs.github.com/en/graphql/reference/enums#reactioncontent

enhancement

This will make it easier to add more events in the future.

Both `ci minimize ci-foo https://...` and `ci minimize ci-foo [description](url)` are supported.

We can probably use https://github.com/actions/upload-artifact/issues/50 / https://docs.github.com/en/free-pro-team@latest/rest/reference/actions#download-an-artifact to get a link to the uploaded artifact(s) from the GH Actions job, and include the URL in the data we send to...

enhancement
bug minimizer

Suggested by @herbelin , I believe, on the feedback survey This plausibly needs some edits on the bug minimizer runner, and we'll need to edit the yml job to have...

bug minimizer

I see things like ``` Error: Unhandled exception: (Invalid_argument Str.matched_group) ``` and similar messages for stack overflow (on logentries), and it would be nice to get a backtrace instead, so...

enhancement

To run the bug minimizer, coqbot creates a branch named run-coq-bug-minimizer-NNNNN. It says something like `Hey NAME, the coq bug minimizer is running your script, I'll come back to you...

enhancement
good first issue
bug minimizer

@JasonGross The documentation of this feature, currently located at https://github.com/coq/coq/wiki/Coqbot-minimize-feature, should probably be updated. BTW, I don't think that the current location for the documentation of this feature is good,...

enhancement
good first issue
bug minimizer