linux-x64.yaml

name: Build and test Pulse
on:
  push:
    branches-ignore:
    - _**
  pull_request:
  workflow_dispatch:
jobs:
  build:
    runs-on: [self-hosted, linux, X64]
    defaults:
      run:
        # Setting the default shell to bash. This is not only more standard,
        # but also makes sure that we run with -o pipefail, so we can safely
        # pipe data (such as | tee LOG) without missing out on failures
        # and getting false positives. If you want to change the default shell,
        # keep in mind you need a way to handle this.
        shell: bash
    steps:
      - name: Record initial timestamp
        run: |
          echo "CI_INITIAL_TIMESTAMP=$(date '+%s')" >> $GITHUB_ENV
      - name: Check out repo        
        uses: actions/checkout@v2
      - name: Identify the base FStar branch and the notification channel
        run: |
          echo "FSTAR_BRANCH=$(jq -c -r '.RepoVersions.fstar' src/ci/config.json || echo master)" >> $GITHUB_ENV
          echo "CI_SLACK_CHANNEL=$(jq -c -r '.NotificationChannel' src/ci/config.json)" >> $GITHUB_ENV
      - name: Determine the build flavor
        run: |
          if docker image inspect fstar:local-branch-$FSTAR_BRANCH ; then echo CI_FLAVOR=hierarchic >> $GITHUB_ENV ; else echo CI_FLAVOR=ci >> $GITHUB_ENV ; fi
      - name: Build Pulse and its dependencies
        run: |
          ci_docker_image_tag=pulse:local-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
          docker build -t $ci_docker_image_tag -f src/ci/$CI_FLAVOR.Dockerfile --build-arg FSTAR_BRANCH=$FSTAR_BRANCH --build-arg opamthreads=$(nproc) . |& tee BUILDLOG
          if ! { echo $GITHUB_REF_NAME | grep '/' ; } ; then
             docker tag $ci_docker_image_tag pulse:local-branch-$GITHUB_REF_NAME
          fi
          docker tag $ci_docker_image_tag pulse:local-commit-$GITHUB_SHA
      - name: Compute elapsed time
        if: ${{ always() }}
        run: |
          CI_FINAL_TIMESTAMP=$(date '+%s')
          CI_TIME_DIFF=$(( $CI_FINAL_TIMESTAMP - $CI_INITIAL_TIMESTAMP ))
          echo "CI_TIME_DIFF_S=$(( $CI_TIME_DIFF % 60 ))" >> $GITHUB_ENV
          echo "CI_TIME_DIFF_M=$(( ($CI_TIME_DIFF / 60) % 60 ))" >> $GITHUB_ENV
          echo "CI_TIME_DIFF_H=$(( $CI_TIME_DIFF / 3600 ))" >> $GITHUB_ENV
          case ${{ job.status }} in
          (success)
            echo "CI_EMOJI=✅" >> $GITHUB_ENV
            ;;
          (cancelled)
            echo "CI_EMOJI=⚠" >> $GITHUB_ENV
            ;;
          (*)
            echo "CI_EMOJI=❌" >> $GITHUB_ENV
            ;;
          esac
          echo "CI_COMMIT=$(echo ${{ github.event.head_commit.id || github.event.pull_request.head.sha }} | grep -o '^........')" >> $GITHUB_ENV
      - name: Output build log error summary
        if: ${{ failure () }}
        run: |
          # Just outputs to the github snippet. Could be part of slack message.
          # This command never triggers a failure, if we did not find anything
          # with grep then we just no-op
          .scripts/fstar_errs.sh BUILDLOG > BUILDLOG_ERRORS || true
          # attach Make error lines, with context
          grep -C10 -E ' \*\*\* ' BUILDLOG >> BUILDLOG_ERRORS || true
          if [ -s BUILDLOG_ERRORS ]; then # if file not empty, report
            ERRORS_URL=$(.scripts/sprang BUILDLOG_ERRORS)
            ERRORS_MSG=" <$ERRORS_URL|(Error summary)>"
            echo "ERRORS_MSG=$ERRORS_MSG" >> $GITHUB_ENV
          fi
      - name: Post to the Slack channel
        if: ${{ always() }}
        id: slack
        uses: slackapi/slack-github-action@v1.16.0
        with:
          channel-id: ${{ env.CI_SLACK_CHANNEL }}
          payload: |
            {
              "blocks" : [
                {
                  "type": "section",
                  "text": {
                    "type": "mrkdwn",
                    "text": "<${{ github.event.head_commit.url || github.event.pull_request.html_url }}|${{ env.CI_COMMIT }}> on (${{ github.ref_name }}) by ${{ github.event.head_commit.author.username || github.event.pull_request.user.login }}"
                  }
                },
                {
                  "type": "section",
                  "text": {
                    "type": "plain_text",
                    "text": ${{ toJSON(github.event.head_commit.message || github.event.pull_request.title || github.run_id) }}
                  }
                },
                {
                  "type": "section",
                  "text": {
                    "type": "mrkdwn",
                    "text": "${{ env.CI_EMOJI }} <https://github.com/${{github.repository}}/actions/runs/${{github.run_id}}|${{ job.status }}>${{env.ERRORS_MSG}}"
                  }
                },
                {
                  "type": "section",
                  "text": {
                    "type": "plain_text",
                    "text": "Duration: ${{ env.CI_TIME_DIFF_H }}h ${{ env.CI_TIME_DIFF_M }}min ${{ env.CI_TIME_DIFF_S }}s"
                  }
                }
              ]
            }
        env:
          SLACK_WEBHOOK_URL: ${{ secrets.SLACK_WEBHOOK_URL }}
          SLACK_WEBHOOK_TYPE: INCOMING_WEBHOOK