coq / bot

A (Coq Development Team) bot written in OCaml

Coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Installation

Please see https://coq.inria.fr/download. Information on how to build and install from sources can be found in INSTALL.md.

Documentation

The sources of the documentation can be found in directory doc. See doc/README.md to learn more about the documentation, in particular how to build it. The documentation of the last released version is available on the Coq web site at coq.inria.fr/documentation. See also Cocorico (the Coq wiki), and the Coq FAQ, for additional user-contributed documentation.

The documentation of the master branch is continuously deployed. See:

• Reference Manual (master)
• Documentation of the standard library (master)
• Documentation of the ML API (master)

Changes

The Recent changes chapter of the reference manual explains the differences and the incompatibilities of each new version of Coq. If you upgrade Coq, please read it carefully as it contains important advice on how to approach some problems you may encounter.

Questions and discussion

We have a number of channels to reach the user community and the development team:

• Our Zulip chat, for casual and high traffic discussions.
• Our Discourse forum, for more structured and easily browsable discussions and Q&A.
• Our historical mailing list, the Coq-Club.

See also coq.inria.fr/community, which lists several other active platforms.

Bug reports

Please report any bug / feature request in our issue tracker.

To be effective, bug reports should mention the OCaml version used to compile and run Coq, the Coq version (coqtop -v), the configuration used, and include a complete source example leading to the bug.

Contributing to Coq

Guidelines for contributing to Coq in various ways are listed in the contributor's guide.

Information about release plans is at https://github.com/coq/coq/wiki/Release-Plan

Supporting Coq

Help the Coq community grow and prosper by becoming a sponsor! The Coq Consortium can establish sponsorship contracts or receive donations. If you want to take an active role in shaping Coq's future, you can also become a Consortium member. If you are interested, please get in touch!

bot's Issues

Automatically merge PR with current base branch instead of asking for a rebase.

Idea from @SkySkimmer. Indeed, it would be good and easy to do I think.

Unhandled artifact failure

There is some code to handle failures at the very end (during artifact upload):

bot/bot.ml

Lines 516 to 535 in b2cd2b7

	(* It could still be a failure that occurred at the very end. *)
	let regex_artifact_fail =
	Str.regexp "Uploading artifacts to coordinator... failed"
	in
	let regex_artifact_success =
	Str.regexp "Uploading artifacts to coordinator... ok"
	in
	let regex_system_failure =
	Str.regexp "Job failed (system failure)"
	in
	if string_match regex_system_failure trace then (
	print_endline "System failure, we'll retry the job.";
	retry_job ~project_id ~build_id
	)
	else if string_match regex_artifact_fail trace
	&& not (string_match regex_artifact_success trace)
	then (
	print_endline "Artifact uploading failure, we'll retry the job.";
	retry_job ~project_id ~build_id
	)

but it is incomplete since it missed this recent example:

https://gitlab.com/coq/coq/-/jobs/85826582

where the trace is:

Running after script...
$ echo "The build completed normally ^(not a runner failure^)."
"The build completed normally (not a runner failure)."
Uploading artifacts...
dev\nsis\*.exe: found 1 matching files             
coq-opensource-archive-windows-*.zip: found 1 matching files 
WARNING: Failed to load system CertPool: crypto/x509: system root pool is not available on Windows 

We can read "Uploading artifacts..." but it stops there, no "Uploading artifacts to coordinator... failed" nor "Uploading artifacts to coordinator... ok".

Management of several open backport projects could be improved.

What to do when multiple stable branches are actively maintained? What rules to enforce? How to combine this with the use of a single milestone per PR.

In the case of PR coq/coq#11197, backporting occurred to v8.10 but it was rejected from v8.11. It shouldn't have been the case and @coqbot should have raised an alert, but its actual reaction was not appropriate.

Possible race when pushing quickly several times to a PR

People can push quickly several times to a PR, especially when using GitHub's suggestion feature, and applying suggestions. If the make-ancestor.sh script is run several times in parallel for the same PR, the script can fail with:

fatal: 'pr-10002' is already checked out at '/tmp/tmp.oKe1DcAZKW'

leading to a wrong conclusion that the current PR cannot be merged with the base branch.

Another race that can also happen in this case is a rebase label being set with a delay. Meanwhile the next push has produced a successful merge which should lead to removing the rebase label if it is set. But it isn't the case yet.

May have broken add milestone to closed issue feature when moving away from ppx_graphql.

The result of the Issue_Milestone query is not correctly parsed by the issue_closer_info_of_resp function which copies the id of the closer's milestone twice in issue_closer_info and closer_info milestone_id fields.

Missed runner failure

https://gitlab.com/coq/coq/-/jobs/86023491

Use a more descriptive title in merge commits

As of today, the bot will merge PRs for the CI with a commit message such as:

Bot merge 28ea4994 into 84b27155

which makes hard to know which is the PR the merge is referring to. I'd be great instead if the bot would add the PR title to the merge commit:

Bot merge 28ea4994 into 84b27155: "Add missing zify class instances"

Use GraphQL for GitLab API calls too.

GitLab's GraphQL API has made much progress recently (https://docs.gitlab.com/ee/api/graphql/reference/index.html) although it still doesn't contain all the mutations we need yet. We should explore whether it is possible to use graphql_ppx with two different GraphQL schema and start using GraphQL for GitLab as well.

Feature request: Support for `needs: bisect`

It would be really nice to be able to have something like the following interaction mode:

1. I add a label needs: bisect to a PR
2. coqbot comments with a template, removes needs: bisect, adds needs: bisect-info
3. I either edit the template from coqbot's comment, or duplicate it into a new comment, and fill it in
4. I remove needs: bisect-info and add needs: bisect-run
5. coqbot runs git bisect run (on GitLab or whatever) based on whatever is in the most-recently-posted comment which matches the template, and when it completes, removes needs: bisect-run, and comments with the final result of bisection, together with a link to the GitLab log.

It would be nice to have special responses for "the versions of Coq you pointed at don't compile", for "the GOOD version of Coq you pointed at fails to compile your file", and for bisect run success.

The template should include a spot for Coq code, a good commit, a bad commit, and a spot for a regex matching the error message, at the very least. If you want, I can clean up my coq-bisect script a bit (basically, have it also build at the bad and good commits you give it, and print a special message if the bad commit succeeds or if the good commit fails), and you could use something like that. My script supports the following environment variables:

• TIMEOUT (default: 30) - how long of a timeout to give to coqc
• FILE - what file to pass to coqc
• ERR_MESSAGE - what string to pass to grep to determine whether or not Coq errored in the way we're bisecting for, or if it had some unrelated failure
• BAD - a tag (e.g., V8.8.1), full branch (e.g., origin/master), or commit hash, for the newer/failing commit
• GOOD - a tag, full branch, or commit hash, for the older/succeeding commit
• CONFIGURE_ARGS - the arguments to pass to ./configure (added to the default arguments of `-local -with-doc no -coqide no -camlp5dir $(ocamlfind query camlp5 | sed s'/ /\ /g')")
• MAKE_TARGET - the arguments to pass to make, e.g., "bin/coqc bin/coqtop theories/Init/Prelude.vo"
• COQTOP_ARGS - the arguments to pass to coqc/coqtop, e.g., "-q"
• SWAP - set this to a non-empty value if the bad commit is older than the good commit (i.e., you want to find where something started working, rather than stopped working)
• EMACS - set this to a non-empty value if the Coq code should be piped to coqtop -emacs, rather than being passed on the command line to coqc.

I'm happy to collaborate on adding support for this feature; if someone else can write the code that communicates to GitHub and GitLab, I can help get my code into shape to support the relevant method of interaction.

Remove surrounding double quotes in result of get_pull_request_refs.

In PR #59, I had to add this trick to make the new feature properly work:

bot/bot.ml

Lines 522 to 523 in d5e7512

	(* Commits reported back by get_pull_request_refs are surrounded in double quotes *)
	when String.equal head.sha (f "\"%s\"" commit) ->

It would be good to remove it by finding the cause for these double quotes and/or stripping them out, but first we should verify that this wouldn't break anything else.

Synchronization sometimes happens with an older version of the pull request

I observed twice a case where a recently updated PR did not have any GitLab-CI status. The bot had been triggered and had pushed the latest version of refs/pull/XXX/head/ to GitLab but it didn't correspond to the latest version of the PR. It seems that there can be a latency in updating this reference. We should be able to fix this by exploiting additional information provided in the webhook's JSON payload: pull_request.head contains an up-to-date sha (together with a ref and a repo.html_url which tells us where to find it).

Interestingly enough, this webhook's JSON payload also contains an outdated pull_request.merge_commit_sha. In the latest occurrence of this bug, the merge commit is coq/coq@f1a374a whose parent is coq/coq@e655947. This was the commit which was pushed to GitLab. On the other hand, the pull_request.head.sha field points to coq/coq@523b549 which is the latest version shown by the PR on GitHub and the one being built by the rest of our CI. For whom it may concern, the X-GitHub-Delivery header for this request is 03ffb460-4ea5-11e8-9e8d-970d83f574ec.

Fix / reenable GitLab build trace checking.

Starting a few days ago, when a CI fails the github widget only displays one entry for the pipeline. Before, it used to additionally give the list of failed processes. This is annoying since it requires opening up the Gitlab interface to check what went wrong, especially since the CI has a tendency to get stuck on launch.

Sometimes coqbot does not add the milestone to an issue.

For instance in coq/coq#10888, @coqbot did not add the milestone of the PR that closed it. When I had the webhook sent again, it worked fine. This could have something to do with the temporary state around the time a PR is merged. In this example, the issue was closed by the PR indirectly (through a commit). If the commit was not properly associated to the PR for a short time, this could have prevented @coqbot from adding the milestone.

coqbot could skim through PRs without assginees and request reviewers to choose an assignee

It could do this for PRs that have been marked as ready-for-review for more than 5 days.

New spurious GitLab CI errors to address

• https://gitlab.com/coq/coq/-/jobs/163235497

  Cloning into '/builds/coq/coq'...
  fatal: unable to access 'https://gitlab-ci-token:[email protected]/coq/coq.git/': The requested URL returned error: 500
  /bin/bash: line 80: cd: /builds/coq/coq: No such file or directory
  ERROR: Job failed: exit code 1
  

• https://gitlab.com/coq/coq/-/jobs/163235488

  Pulling docker image gitlab/gitlab-runner-helper:x86_64-35e8515d ...
  ERROR: Job failed: execution took longer than 4h0m0s seconds
  

• https://gitlab.com/coq/coq/-/jobs/163235500

  Pulling docker image gitlab/gitlab-runner-helper:x86_64-7a7b8375 ...
  ERROR: Job failed: canceled
  

dune build --ignore-promoted-rules seems to not be working anymore

Running dune build --ignore-promoted-rules with no bot-components/.github-token was supposed to succeed and now it gives the following error message:

File "bot-components/dune", line 19, characters 0-187:
19 | (rule
20 |  (targets .graphqlconfig)
21 |  (deps
22 |   (:input .graphqlconfig.in)
23 |   .github-token)
24 |  (action
25 |   (with-stdout-to
26 |    %{targets}
27 |    (run sed "s/%%TOKEN%%/%{read:.github-token}/" %{input}))))
Error: No rule found for bot-components/.github-token

@coqbot could automatically run benchmarks

@coqbot is already following the pull request webhook and thus it is aware of every "labeling" event in particular.
When it sees the "needs: benchmarking" label, it could automatically run the bench, and when it finishes, it could post the results as a comment and remove the label.

Before implementing this, I'd like to understand better the future of the benchmark infrastructure. Is it going to stay on Jenkins or could we move it to GitLab CI somehow and kill Jenkins completely?

Job failures are not reported when project name differs from project slug on GitLab.

With @jtcoolen, we noticed that a project on GitLab can have a name which doesn't reflect correctly the project URL. In this case, the status checks for failed GitLab CI jobs are not reported to the right URL on GitHub.

Remove dependency on ppx_graphql.

Now that we depend on graphql_ppx_re, the only actively maintained OCaml / ReasonML GraphQL ppx (for typed GraphQL requests), we should be able to stop depending on the unmaintained ppx_graphql library. But the dependency has been kept for now because of one request (cf. bot-components/GitHub_queries_bis.ml) which is not yet supported by graphql_ppx_re. We should patch the library, or workaround the issue, to drop the dependency on ppx_graphql.

Note that as ppx_graphql depends on the deprecated package ppx_metaquot, its use is blocking an upgrade from OCaml 4.06 to OCaml 4.07.

fatal: could not read Username for 'https://github.com': No such device or address

I've ran into the limitations of Gitlab CI/CD with an external repository (GitHub) setup and came across this coqbot from https://gitlab.com/gitlab-org/gitlab-ee/issues/5667. I've run into a brickwall in terms of setting up my own coqbot. Opening a GitHub PR seems to be just giving me this:

2019-07-25T15:13:45.579655+00:00 heroku[router]: at=info method=POST path="/github" host=bfung2b.herokuapp.com request_id=2d7b1a25-e75f-4faa-96f8-6afba6f2aefd fwd="140.82.115.71" dyno=web.1 connect=0ms service=3ms status=200 bytes=129 protocol=https
2019-07-25T15:13:45.714545+00:00 app[web.1]: fatal: could not read Username for 'https://github.com': No such device or address

Any guidance would be greatly appreciated!

@coqbot sometimes miss some outdated PRs.

Today at 17:26 (+0200), it was "working": here is an outdated PR that got a need: rebase label:

{
  "action": "synchronize",
  "number": 7878,
    "head": {
      "label": "maximedenes:omega-lia",
      "ref": "omega-lia",
      "sha": "e3c02c83817f6264c44c1a05acd87513d207e78b"
    },
    "base": {
      "label": "coq:master",
      "ref": "master",
      "sha": "4ab54f3cca76632cb6e258c84abc259e15e9e9f8"
    }
}

(webhook request identifier: 160dcff0-901f-11e8-92fb-4f4bf88c7c85)

At the time of pushing coq/coq@4ab54f3 was indeed already outdated. It seems however that it wasn't the actual (also outdated commit) on which this PR was based (coq/coq@e3c02c8 closest parent in master seems instead to be coq/coq@32415df).

But at 17:55 (+0200), it was broken: here is an outdated PR that was not caught:

{
  "action": "synchronize",
  "number": 891,
    "head": {
      "label": "mattam82:check_univ_decls",
      "ref": "check_univ_decls",
      "sha": "cba9f3fe48817e8e524483fd984ea4938b3dc14f"
    },
    "base": {
      "label": "coq:master",
      "ref": "master",
      "sha": "523de4f878293cf1d582bd70300b34d497e705b3"
    }
}

(webhook request identifier: 2d775310-9023-11e8-99fb-295ac80be283)

Several other occurrences of this problem afterwards.

coq/coq@523de4f was the head of master at the time while the closest parent of coq/coq@cba9f3f to be in master is coq/coq@9b6ce4f.

Other, older (16:23), and wrong example:

{
  "action": "opened",
  "number": 8142,
    "head": {
      "label": "Zeimer:fix-chapter-syntax-extensions",
      "ref": "fix-chapter-syntax-extensions",
      "sha": "51f887aa9476ddf036499bca5f7728a0ec3ac221"
    },
    "base": {
      "label": "coq:master",
      "ref": "master",
      "sha": "523de4f878293cf1d582bd70300b34d497e705b3"
    }
}

(webhook request identifier: 425cd320-9016-11e8-93a6-ea1050b264a2)

coq/coq@51f887a was based on an older version of master (coq/coq@32415df) while coq/coq@523de4f was the current head of master at the time.

Overall, the conclusion seems to be that the base.sha info cannot be trusted.

Add failed status check to the "needs: rebase" label.

So that contributors realize that GitLab CI won't run until the PR is rebased.

Timeouts should not be counted as runner failures

Because consistent timeouts can also be caused by significant slowdowns.

Could coqbot help to enhance GitLab CI integration in GitHub "Checks" tab?

With coqbot the GitHub / GitLab CI integration in PRs is very fine!

But I've just noticed that some GitHub feature was not handled though, the Checks tab is currently empty: https://github.com/math-comp/math-comp/pull/524/checks (see screenshot below).

Screenshot

to be compared with e.g. that of Travis CI,

or that of GitHub Actions.

Of course:

• this feature suggestion is not crucial at all
• maybe this should/could be handled by GitLab CI itself

but if GitLab doesn't plan to implement this (which has to be handled by a dedicated GitHub app? or maybe via an API call, I didn't have a look), coqbot might help at some point? (provided it is easy to implement this with the current architecture)

@coqbot could report failures from GitLab CI and restart spurious ones

When a GitLab CI pipeline completes with failures, first check if the pipeline is up-to-date with respect to the PR.

If yes, check if some of the failures are spurious:

• "runner system failure" detected by GitLab, example error message: ERROR: Job failed (system failure): Cannot connect to the Docker daemon at tcp://10.142.0.123:2376. Is the docker daemon running?
• connection trouble:

  error: RPC failed; HTTP 500 curl 22 The requested URL returned error: 500 Internal Server Error
  fatal: The remote end hung up unexpectedly
  ERROR: Job failed: exit code 1
  

• uploading artifacts failed:

  Uploading artifacts to coordinator... ok            id=71082452 responseStatus=201 Created token=G7Azf-fN
  ERROR: Job failed: exit code 1
  

If yes, restart the corresponding jobs.
(For the spurious failures we have control upon, we should fix them instead.)

Otherwise, post a message in the PR thread with the last few lines of the failing job logs and direct links to these logs.

[wish] links for stdlib html

Dear bot, I'd like to have a link to the stdlib, eg
https://coq.gitlab.io/-/coq/-/jobs/132518399/artifacts/_install_ci/share/doc/coq/html/stdlib/index.html
It is built by the doc:refman job, but the status link only points to the output of sphinx.

@coqbot could handle a lot of the release management taks.

The current release process includes creating a release issue (cf. coq/coq#8445, coq/coq#8446, coq/coq#10843, coq/coq#11157, coq/coq#12334). These issues were created by copy-pasting the content of dev/doc/release-process.md.

Some steps in this checklist could be entirely automated. It would be great if @coqbot could take care of them whenever we check a box. This would include creating the missing milestone, the backporting project, opening the PR bumping the version numbers, opening the PR consolidating the release notes, and even creating the next release issue from the release process doc.

Some actions like pushing tags should not be done when checking boxes (which can happen accidentally) but when merging PRs doing version number bumps instead. The release branch could also be created automatically upon merging the next alpha bump in master.

Automatically run opam-publish.

The bot could listen to branch / tag creation webhooks. When a new tag is created in a repository which contains an opam file, it could run opam-publish to update the corresponding package on opam-coq-archive. Webhooks can be installed on individual repositories or organization-wide, so it should be very easy to support all repositories in an organization such as coq-community (or coq-contribs if the repositories contained opam files). Upon PR creation, the bot would ping the tag creator (and possibly also all listed maintainers if the repository contain a meta.yml with this information) to check the PR.

Note that I have never used opam-publish so I might be a little naive about it.

Initially proposed in coq/opam#500 (comment).

@coqbot could post the link to the documentation artifact for PRs labeled "documentation"

Or to be even more precise, we could create a part: refman label.

When trace exceeds the size limit, the job should not be retried

Example here: https://gitlab.com/coq/coq/-/jobs/86816584

Monitor newly created branches and tags and immediately delete non-conforming ones.

Typically, we only want to allow branches in the form vX.X and master and signed tags in the form VX.X.X, VX.X+alpha, VX.X+betaX.

coqbot logs are too verbose

Because of this verbosity, I can't go back many hours back to explore a problem as Heroku only stores the last 1500 log lines.

Coqbot could tag stale CI builds in PR as `needs: rebase`.

see: coq/coq#7718

mergify/bors-like merging process

This would ensure better reliability because CI would run on commits before they become the HEAD of master or a stable branch.

This would however require first a (planned) change to the way overlays are handled (cf. coq/coq#6724).

There is also a question on how to allow the pkg:nix job to upload its result to Cachix (the CACHIX_SIGNING_KEY secret variable is only available on protected branches, but it could also be passed to a triggered pipeline).

More generally, do we want the staging branch to be protected (in which case there will be a number of staging branches) or is it OK to force-push to staging? Do we need the staging branch to appear on the GitHub repository or can it be only pushed to GitLab? If we could gather all of Coq CI on GitLab (we are not so far), then there would be no point in pushing to the GitHub repository (there is also the option of triggering external CI from GitLab CI).

Configuration file

Should be useful for a number of things:

• set the correspondence between GitLab repo and GitHub repo;
• activate various features beyond the synchronization feature;
• set a team of trusted contributors (see #33)
• etc.

Support other projects that want to push PRs to GitLab

GitLab CI is a great CI platform that can be used for GitHub projects too (thanks to CI/CD-only project mirroring). The only thing that is lacking is building pull requests (it only mirrors branch). In Coq, we use the present bot to push all new or updated PRs to branches that are named pr-<number> to GitLab (and we deleted them when the corresponding PR is closed). This is enough to have CI run for PRs (GitLab takes care of reporting back the status of the build). Other projects could be interested to use this capability as well. How to support them?

• The first solution is to support them on a case by case basis by having the bot listen to webhooks from other repositories and pushing to other repositories. This is easy to do in practice.
• The second solution is to provide a library of reusable GitHub / GitLab bot components with enough documentation so that other projects can easily have their own bot up and running (this is the plan).
• The third solution is to provide a "GitHub action" whenever these get actually released to all projects: https://github.com/features/actions. This could be set up more easily, with personalized workflows and does not require deploying on Heroku.

Please support `allow_failure: true` for GitLab CI jobs.

Dear coqbot developers,

In coq/coq#8546 a job with the allow_failure property set to true did indeed fail, but the bot is not aware of that and thus marking the whole PR as failed.

Please support such use case by filtering out jobs that carry such tag.

When a merged PR automatically closes an issue, put the issue in the same milestone.

If the issue was not in any milestone, @coqbot will add the issue to the same milestone.
If the issue was in another milestone, @coqbot will post a warning in a message.

Pending on improvements from GitHub to the issue webhook.

Connectivity issues should probably be tagged as runner failures and re-tried

See https://gitlab.com/coq/coq/-/jobs/81764255:

+ git clone --depth 1 https://github.com/mit-plv/cross-crypto .
Cloning into '.'...
fatal: unable to access 'https://github.com/mit-plv/cross-crypto/': transfer closed with outstanding read data remaining
Makefile.ci:62: recipe for target 'ci-cross-crypto' failed
make: *** [ci-cross-crypto] Error 128
Running after script...
$ echo "The build completed normally (not a runner failure)."
The build completed normally (not a runner failure).
ERROR: Job failed: exit code 1

@coqbot can help with backporting

• When a PR is merged, if the milestone description contained "coqbot: backport to BRANCH (request inclusion column: URL1 / backported column: URL2)", and the PR was not targeting BRANCH already, then put the PR in the project column URL1.
• When new commits are pushed, if their message is "Backport #PRNUM..." or "Merge #PRNUM..." and the description of the milestone for the corresponding PR contained the above text, then put / move these PRs to the project column URL2.
• At the time of putting a PR in the request inclusion column, backport this PR to the backport branch of @coqbot's fork of the Coq repository (if it can be done without solving conflicts) and open a PR for this branch if the branch didn't exist (and delete the branch whenever the corresponding PR is merged).

GitHub Action

Would it be possible to use this in a GitHub Action to sync PRs from GitHub to GitLab? It'd make it a lot easier to get started and wouldn't require relying on the Coq bot Heroku app.

Feature: comment with rendered doc

It'd be nice to have coqbot comment with either a diff of the html output of the doc, or with the rendered version of any sections that change. Presumably the former is easier; it could download the doc from whatever artifacts have them, and comment with the diff.

Ideally, it should comment only if there is a change to anything in the doc/ folder, and it should update its existing comment (if it exists) whenever a push is made to the PR / whenever the doc pipeline completes.

Add/Remove pull request from backporting project when its milestone is updated.

In particular, when a milestone is removed, the issue event with action "demilestoned" provides the previous milestone as a top-level value, and the new milestone as a child of the issue value (however, it doesn't contain the info whether the pull request has been merged).

Authenticating to GitHub's API using username + password is deprecated.

All indirect uses of the following line to communicate with the GitHub API should be removed:

bot/bot.ml

Line 13 in e527d05

let credentials = `Basic (username, password)

The GitHub access token should be used instead of the password.

More info at https://developer.github.com/v3/auth/#basic-authentication

Recent failure to push a PR to GitLab

It seems that there is a pre-receive hook at gitlab.com/coq/coq (probably a default pre-receive hook) that failed because of some internal error and prevented to push a PR to GitLab. Relevant logs:

2018-05-07T15:52:44.307834+00:00 app[web.1]: From https://github.com/Zimmi48/coq
2018-05-07T15:52:44.307856+00:00 app[web.1]:  * branch            clean-up/internal-function -> FETCH_HEAD
2018-05-07T15:52:45.757916+00:00 app[web.1]: remote: hooks/pre-receive:19:in `increase_reference_counter': undefined method `[]' for nil:NilClass (NoMethodError)        
2018-05-07T15:52:45.757933+00:00 app[web.1]: remote: 	from hooks/pre-receive:32:in `<main>'        
2018-05-07T15:52:45.776715+00:00 app[web.1]: To [email protected]:coq/coq
2018-05-07T15:52:45.776723+00:00 app[web.1]:  ! [remote rejected] 40c97a2c23e7f6c49b8812346c2e05190ed6f496 -> pr-7450 (pre-receive hook declined)
2018-05-07T15:52:45.776726+00:00 app[web.1]: error: failed to push some refs to '[email protected]:coq/coq'
2018-05-07T15:52:45.778633+00:00 app[web.1]: Command "cd ~/repo && GIT_SSH_COMMAND='ssh -i ~/bot_rsa -o "StrictHostKeyChecking=no"' git fetch https://github.com/Zimmi48/coq clean-up/internal-function && cd ~/repo && GIT_SSH_COMMAND='ssh -i ~/bot_rsa -o "StrictHostKeyChecking=no"' git push [email protected]:coq/coq +40c97a2c23e7f6c49b8812346c2e05190ed6f496:refs/heads/pr-7450" exited with status 1.

To investigate and maybe open a bug report at GitLab.

Feature: trusted contributors

When managing your own CI runners, it might not be desirable to let just anyone execute arbitrary code on it by creating a PR. Instead, a project might mark a number of regular contributors as trusted. Contributors marked as trusted would see their PRs automatically tested, while others need manual approval.

Two implementation strategies I can think of:

1. the bot could lookup the members of a specific team within the organization and consider them trusted
2. trusted users could be hardcoded through command line arguments

Would this fit within the scope of this project?

Autoposting documentation links

It'd be really cool if coqbot could post a link to the CI-generated documentation for PRs that touch any of the doc files (at least whenever the doc job succeeds). Bonus points if the link(s) point exactly to the pages that were changed in the PR. I found myself wanting this at coq/coq#12129 (comment)

Merging with @coqbot.

This was already mentioned as a first step to #18 but let's make an issue just for it.

The idea is to support merging with @coqbot (and maybe later on remove the merging script).

The process would be to write "@coqbot: merge now" within a comment.

As with the merging script, the bot would check a few things:

• the PR targets the master branch
• the user asking to merge is among the assignees, is in the pushers team and is not the author of the PR
• there are no request for changes
• there is a kind label
• there are no needs labels
• there is a milestone

and would abort with a comment if any of these checks fail.

It would also check that CI passed and if it's not the case it would ask confirmation.
The user asking to merge the PR could skip the confirmation step by adding "Ignore CI failures" to the comment requesting to merge.

If the PR has overlays (i.e. files in directory dev/ci/user-overlays), @coqbot should post a comment to remind the merger to take care of those.

Improving reporting on failed builds.

In coq/coq#9278, @Zimmi48 has done some preliminary preparation to better understand failures of CI runs. IMHO that'd be very useful and I can see several tasks here, for example, the bot could link to the exact point of the log where the error happened.

Feature: check PRs for merge conflicts

Maybe on a timer rather than every merge.