Bryan Gin-ge Chen
Bryan Gin-ge Chen
This looks reasonable, though I haven't done a full review yet. Do you mind updating the `README` and adding a test or two?
It just happened again; right after I added `bors r+` to a PR. Mon, 04 Oct 2021 19:34:32 GMT: ```elixir {:timeout, {GenServer, :call, [ BorsNG.GitHub, {:get_file, {{:installation, 7893283}, 97922418}, {"a4e020c654a8763cd2d763c0c49938c4d380bda0",...
Thanks for looking into this! I've closed that PR and I'll put the other ones back on the queue.
I don't think so. It looks like what happened was a merge commit [4c62797](https://github.com/leanprover-community/mathlib/pull/5672/commits/4c62797c80a56eeb0b7179f9b38ea9b306d3562a) was pushed to that branch and bors said "Canceled" in the comment linked above. However for...
I just ran into the lack of error-reporting in the worker builds as well. If it helps narrow things down, I've confirmed that the non-worker builds do throw errors properly...
Is the base of this PR supposed to be the branch for #4315 or should it be `master`?
@EdAyers added documentation in https://github.com/leanprover-community/lean/pull/443.
I agree that we're not actually using the markdown files as templates, and I tried to figure out how to disable the checking but it seemed like it would require...
Note to myself or to anyone who eventually does this: don't forget to replace `Kha/elan` with `leanprover/elan` in the workflow.
@b-mehta do you mind adding the module docstring? We can see if anyone wants to rewrite the proof steps afterwards.