A multi-function bot, written in OCaml

Most of the functions of this bot are used in the development of Coq.A subset of functions (most notably the ability to synchronize GitHubpull requests to GitLab branches and report back the results ofcontinuous integration) are used in dozens of additional projects.

This is a work in progress and your help is welcome, both in the formof issues and pull requests. When reporting a bug or requesting afeature, please be as specific as possible, and be ready to follow up.If you are not ready to follow up to make your needs more explicit, orto help with testing, don't bother requesting a new feature in thefirst place.

Contents

1. Features
2. How to use the @coqbot instance
3. Architecture
4. How to deploy a new instance
5. Building locally

Features

Synchronization between GitHub and GitLab

GitLab is not just a development platform similar to GitHub, it isalso one of the best CI providers there is today. Consequently, it isno surprise that many projects that are developed on GitHub want touse GitLab for CI/CD. Since 2018, GitLab CI/CD supportsGitHub, but this only means mirroring therepository's branches and reporting status checks back. Pull requestsoriginating from forks get no testing, even though this has been afeature request for more than two years.

Synchronize pull requests from forks

This bot works around this issue by pushing new and updated pullrequests to branches on the GitLab mirror. Note that depending onyour settings this could result in a security risk. In particular, ifyou have secret variables, you should restrict them to protectedbranches. Otherwise, anyone could instrument pull request testing toget access to their values.

Automatic merge commits for testing

Like Travis, the bot always create a merge commit of the pull requesthead with the head of the base branch, which is very convenient whenthe pull request is not up-to-date with the base branch. If theautomatic merge fails, then the bot will push a failed status check onthe PR and set a "needs: rebase" label (if this labels exists). Italso removes the label when an updated version without conflicts ispushed.

Detailed failure reporting

In the reverse direction, the bot will substitute itself to the statuscheck reporting that GitLab supports, and report more detailedinformation on failing pipelines (with a direct link to the failedjobs).

Using the status check reporting provided by this bot rather than theone provided by GitLab is essential, because GitLab wouldn't know howto report the status back for automatic merge commits.

GitHub Checks features

When the bot is installed as a GitHub App, it usesthe GitHub Checks tab for the status reporting. You get someadditional benefits, like having a snippet of the failed build logsand the ability to restart failed jobs and pipelines by clicking onthe "Re-run" button.

The GitHub App is also able to report failed jobs in allow_failuremode as "neutral" status checks.

Other GitHub-GitLab synchronization features

The bot can also add direct link to artifacts generated by the CI toease reviewing. For now, this feature is only activated on the Coqrepository. Please open an issue if you would like to use it on yourrepository too.

The bot will delete branches corresponding to pull requests when thepull requests are merged or closed.

Finally, the bot handles some cases of spurious failures byrelaunching the failed job automatically, for instance in case ofrunner failure. At some point in the past, shared runner failureswere very frequent and this feature was absolutely necessary to makeGitLab CI/CD usable in practice.

Please open an issue if you would like any of the behaviors describedabove to be configurable.

Clear milestone of unmerged pull requests

When a pull request is closed without being merged, the bot willremove any milestone that had been set.

Please open an issue if you would like this behavior to beconfigurable.

Mark pull request as stale and automatically close them

If this feature is used, the bot will mark pull requests as stale whenthey have not been rebased for more than 30 days, with a commentgiving another 30 days to rebase the pull request before it isautomatically closed.

To use the feature, create the needs: rebase and the stale labelsand set up a cron job (e.g. a scheduled GitHub Action) to call the/check-stale-pr endpoint every day with owner:repo in the body.

This feature is best used in combination with a GitHub Action toautomatically add the needs: rebase label when a conflict appearsafter the base branch has been updated. Example:

name: "Check conflicts"
on: [push]
# Only on push because @coqbot already takes care of checking for
# conflicts when PRs are opened or synchronized

jobs:
  main:
    runs-on: ubuntu-latest
    steps:
      - uses: eps1lon/actions-label-merge-conflict@b8bf8341285ec9a4567d4318ba474fee998a6919
        with:
          dirtyLabel: "needs: rebase"
          repoToken: "${{ secrets.GITHUB_TOKEN }}"

Synchronize closed issue's milestone with the one of the pull request that closed it

If an issue is closed automatically when merging a pull request, andthis pull request had a milestone set, then the bot will add the issueto the same milestone. If the issue was already in a differentmilestone, the bot will change the milestone and post a commentalerting of the change.

This feature won't be activated if you don't select the "issue" eventwhen configuring the GitHub webhook. However, it is activated if youinstalled the bot as a GitHub App. Please open anissue if you would like this behavior to be configurable.

Post comment when a pull request does not respect certain standards

This feature is only activated on the Coq repository. Please open anissue if you would like to use it on your repository too.

When someone opens a pull request but the name of the branch that wasused to open the pull request is the same as the base branch, the botposts a comment recommending to do differently next time, and suggestsreading the contributing guide.

Manage the backporting process

This is a complex feature that is not activated by default, and thatwould deserve a whole document to present it. Please open an issue ifyou are interested in hearing about it.

How to use the @coqbot instance

As a GitHub App

This is the recommended installation method, as this is both easier toset up and it gives access to new features (related to GitHub Checks).

Notes:

• Installation as a GitHub App is still in an experimental stageand you may frequently receive requests to expand permissions.

• All the repositories that use the bot and belong to the sameowner must install the bot using the same method (GitHub App orregular user).

• If you were previously using the legacy installation method,make sure you disable any previously set up GitHub webhooks whenswitching to the GitHub App, otherwise the bot will receive everyrequest twice.

The bot can be installed as a GitHub App to either your account ororganization (link to app).Once you finish the installation, follow these steps:

• Create a repository on GitLab.com which will be used to run CI jobs.

  The bot will only take care of mirroring the PRs and reportingstatus checks back so you may still want to activate the mirroringfeature for the main branches. To do so, the easiest way is tochoose the "CI/CD for external repo" option when creating the GitLabrepository. However, you should opt to give the repo by URL ratherthan with the GitHub button, because we won't need GitLab's ownstatus check reporting feature. (If it is already activated, you candisable this integration in the "Settings" / "Integration" menu).

• In your GitLab repository:

  • go to "Members" to add@coqbot as a project member with"Developer" role (so that it can push new branches).

  • go to "Settings" / "Webhooks" and create one webhook that will betriggered by pipeline events and job events. Set its URL tohttps://coqbot.herokuapp.com/gitlab.

  By default, @coqbot considers that both GitHub and GitLab repositoriesshare the same URL except for the "lab" replacing the "hub" part. Ifthat is not the case, assuming you created a GitLab repository whoseURL is https://gitlab.com/owner/repo/, add a file coqbot.toml atthe root of your GitHub repository and in its default branch (most oftennamed master), containing:

  [mapping]
  gitlab = "owner/repo"
  

  If you use other instance of @coqbot, this repository-specificconfiguration file becomes BOT_NAME.toml where BOT_NAME is the nameof the bot.

As a regular user account (legacy)

The bot used to be given access to each of your GitHub repositories as aregular GitHub user account (@coqbot). This installation method isstill supported for repositories that haven't migrated to the GitHub Appyet. Here are the steps to follow in addition to those described in theAs GitHub App section:

• In your GitHub repository:

  • go to "Settings" / "Manage access" to add@coqbot as a collaborator withthe "Write" role (so that it can push status checks, and setlabels).

    Currently, every invitation requires a manual validation, so theremay be some lag before @coqbot can push status checksto your repository.

  • go to "Settings" / "Webhooks" and add one webhook with URLhttps://coqbot.herokuapp.com/github that will only be triggeredat least by pull request events, and if you want to use the issuemilestone feature, by issue events as well. Make sure you changethe "content/type" value to "application/json".

Architecture

The bot has grown according to the needs for automation in the Coqproject, initially as a single file, and is now incrementally beingrearchitected around the idea of providing a library of base botcomponents that can be used in a trigger-action programming model.

The most popular trigger-action programming platforms as of today areIFTTT and Zapier. Interestingly both of them provide a GitHubintegration, and Zapier provides a GitLab integration as well, buttheir integrations do not include sufficiently advanced triggers noractions to perform the kind of things that this bot does.

The bot components are of three types (the naming follows GraphQL'sterminology of the corresponding GraphQL requests,GraphQL requests are preferred to REST requests whenever possible):

• Subscriptions are the events that the bot listens to (currentlyGitHub and GitLab webhooks). See for instancebot-components/GitHub_subscriptions.ml.

• Queries are the requests that are sent to gather additionalnecessary information, and to decide whether the conditions toperform an action are met. See for instancebot-components/GitHub_queries.ml.

• Mutations are the state-changing actions that are performed bythe bot, in response to some event and some conditions being met.See for instance bot-components/GitHub_mutations.ml.

When this architecture is sufficiently stable, the goal is to publishthe bot-components folder as an independent library of buildingblocks to create a personalized bot in OCaml. In the meantime, if youdeploy your own instance, the callback function in the bot.ml fileis the main entry point, where you can decide of your businesslogic by choosing the subscriptions you listen to, and by triggeringthe relevant queries and mutations on demand.

How to deploy a new instance

Creating an instance of the bot requires to create aGitHub App and set up a server.

Deploying the server

We provide a Docker image at each release, which can be easily deployedto Heroku. Simply follow the officialinstructions.

The bot will need to read a few environment variables so make surethese are configured in your Heroku app:

• GITLAB_ACCESS_TOKEN
• GITHUB_ACCESS_TOKEN
• GITHUB_WEBHOOK_SECRET
• GITHUB_PRIVATE_KEY (a private key of your GitHub app)
• GITHUB_APP_ID (your GitHub App ID)

Then, you must configure the bot with a configuration file. Here is an exampleto adapt to your needs example-config.toml).

Here is an example of Dockerfile to build a personalized image basedon a release image from GitHub packages, using a custom bot_config.tomlconfiguration file:

FROM docker.pkg.github.com/coq/bot/coqbot:v0.2.0

COPY path/to/bot_config.toml ./

EXPOSE 8000 # The port you specified in bot_config.toml
            # (this command is ignored if you deploy to Heroku)

CMD ["./bot.exe", "bot_config.toml"]

Keep in mind that you should login first to GitHub packages with yourGitHub credentials.

Create a GitHub App

Please follow the instructionsfor creating a GitHub App.

Make sure to enter the address of your instance of the server followed by /github in theWebhook URL entry. It typically looks like https://myapp.herokuapp.com/github if youdeployed the server to Heroku.

You can also specify the Webhook Secret, which should correspond to the GITHUB_WEBHOOK_SECRETenvironment variable.

Then, you need to set the following permissions:

• Repository permissions:

  • Checks: read & write
  • Contents: read & write
  • Issues: read & write
  • Metadata: read-only
  • Pull requests: read & write
  • Projects: read & write
  • Commit statuses: read & write

• Organization permissions:

  • Members: read-only
  • Projects: read & write

• Subscribe to events (check the following events):

  • Check run
  • Commit comment
  • Create
  • Issue comment
  • Issues
  • Project
  • Project card
  • Project column
  • Pull request
  • Pull request review
  • Push

Building locally

Instructions for building and testing locally can be found in thecontributing guide.