Use GitHub Actions to place a MyBinder.org badge on pull requests

You can facilitate review of GitHub pull requests on mybinder.org by using GitHub Actions to place a Binder badge or link on Pull Requests. Below are several examples of how to accomplish this.

To enable GitHub Actions, you must place .yaml files that define your GitHub Action workflow in the /.github/workflows/ directory in your repository.

Example 1: Comment on pull request with a binder badge

The below action uses the github/script Action to call the GitHub API for the purposes of making a comment on a PR that looks like this:

Binder 👈 Launch a binder notebook on this branch for commit xxxxxxx

Download the below file: binder-badge.yaml

#./.github/workflows/binder-badge.yaml
name: Binder Badge
on: [pull_request_target]

jobs:
  binder:
    runs-on: ubuntu-latest
    steps:
    - name: comment on PR with Binder link
      uses: actions/github-script@v1
      with:
        github-token: ${{secrets.GITHUB_TOKEN}}
        script: |
          var PR_HEAD_USERREPO = process.env.PR_HEAD_USERREPO;
          var PR_HEAD_SHA = process.env.PR_HEAD_SHA;
          github.issues.createComment({
            issue_number: context.issue.number,
            owner: context.repo.owner,
            repo: context.repo.repo,
            body: `[![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/gh/${PR_HEAD_USERREPO}/${PR_HEAD_SHA}) :point_left: Launch a binder notebook on this branch for commit ${PR_HEAD_SHA}`
          })
      env:
        PR_HEAD_SHA: ${{ github.event.pull_request.head.sha }}
        PR_HEAD_USERREPO: ${{ github.event.pull_request.head.repo.full_name }}

Example 2: Comment with a Binder badge in response to a comment

In the below example, we will trigger GitHub Actions to run after someone comments on a pull request with the command /binder, which will trigger Actions to comment on a PR in the same way as Example 1.

Download the below file: chatops-binder.yaml

#./github/workflows/chatops-binder.yaml
name: Chatops Binder
on: [issue_comment] # issues and PRs are equivalent in terms of comments for the GitHub API

jobs:
  trigger-chatops:
    # Make sure the comment is on a PR, and contains the command "/binder"
    if: (github.event.issue.pull_request != null) &&  contains(github.event.comment.body, '/binder')
    runs-on: ubuntu-latest
    steps:
      # Use the GitHub API to: 
      #  (1) Get the branch name of the PR that has been commented on with "/binder" 
      #  (2) make a comment on the PR with the binder badge
    - name: comment on PR with Binder link
      uses: actions/github-script@v1
      with:
        github-token: ${{secrets.GITHUB_TOKEN}}
        script: |
          // Get the branch name
          github.pulls.get({
            owner: context.repo.owner,
            repo: context.repo.repo,
            pull_number: context.payload.issue.number
          }).then( (pr) => {

            // use the branch name to make a comment  on the PR with a Binder badge
            var BRANCH_NAME = pr.data.head.ref
            github.issues.createComment({
              issue_number: context.payload.issue.number,
              owner: context.repo.owner,
              repo: context.repo.repo,
              body: `[![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/gh/${context.repo.owner}/${context.repo.repo}/${BRANCH_NAME}) :point_left: Launch a binder notebook on this branch`
            })
          })

Permissions

You may want to restrict who can trigger a binder badge to be created by their association with a repository. When triggering GitHub Actions on an issue_comment event, you can access the association of the person who opened the pull request with the variable github.event.issue.author_association and the person commenting on the pull request with github.event.comment.author_association.

Note

An issue_comment event is triggered when you comment on a pull request. This is because the GitHub API treats issues and pull requests as the same entity in many places. This is also why you can access the association of the person who opened the pull request with the github.event.issue.author_association when the issue_comment event occurs.

Similarly, when triggering GitHub Actions on a pull_request event, you can access the association of the person who opened the pull request with the variable github.event.pull_request.author_association.

For example, this is how you can conditionally trigger the workflow shown in Example 1 if the person opening the PR is a OWNER, COLLABORATOR, MEMBER, or CONTRIBUTOR:

Download the below file: binder-badge-permissions.yaml

#./github/workflows/binder-badge-permissions.yaml
name: Binder Badge
on: [pull_request]

jobs:
  binder:
    if: |
      (
        (github.event.issue.author_association == 'OWNER') ||
        (github.event.issue.author_association == 'COLLABORATOR') ||
        (github.event.issue.author_association == 'CONTRIBUTOR') ||
        (github.event.issue.author_association == 'MEMBER')
      )
    runs-on: ubuntu-latest
    steps: 
    - name: comment on PR with Binder link
      uses: actions/github-script@v1
      with:
        github-token: ${{secrets.GITHUB_TOKEN}}
        script: |
          var BRANCH_NAME = process.env.BRANCH_NAME;
          github.issues.createComment({
            issue_number: context.issue.number,
            owner: context.repo.owner,
            repo: context.repo.repo,
            body: `[![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/gh/${context.repo.owner}/${context.repo.repo}/${BRANCH_NAME}) :point_left: Launch a binder notebook on this branch`
          }) 
      env:
        BRANCH_NAME: ${{ github.event.pull_request.head.ref }}

Further Reading

There are many more ways you can customize your workflows to suit your needs. Please see the official GitHub Actions documentation for more information.