linux-x64-rebuild-base.yaml

name: Rebuild base image
on:
  schedule:
    # 2AM UTC
    - cron: '0 2 * * *'
  workflow_dispatch:
    inputs:
      force:
        description: Update the base image even if running F* CI fails, and even if this branch is not master
        required: true
        type: boolean
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: Check out repo
        uses: actions/checkout@v3

      - name: Rebuild base image from scratch
        run: |
          TEMP_IMAGE_NAME=fstar:update-base-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
          CI_IMAGEBUILD_INITIAL_TIMESTAMP=$(date '+%s')
          docker build --pull --no-cache -f .docker/base.Dockerfile -t ${TEMP_IMAGE_NAME} .
          CI_IMAGEBUILD_FINAL_TIMESTAMP=$(date '+%s')
          echo "CI_IMAGEBUILD_INITIAL_TIMESTAMP=$CI_IMAGEBUILD_INITIAL_TIMESTAMP" >> $GITHUB_ENV
          echo "CI_IMAGEBUILD_FINAL_TIMESTAMP=$CI_IMAGEBUILD_FINAL_TIMESTAMP" >> $GITHUB_ENV
          echo "TEMP_IMAGE_NAME=$TEMP_IMAGE_NAME" >> $GITHUB_ENV

      - name: Check that F* CI passes
        run: |
          echo "CI_INITIAL_TIMESTAMP=$(date '+%s')" >> $GITHUB_ENV
          ci_docker_image_tag=fstar:update-base-test-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
          echo "ci_docker_image_tag=$ci_docker_image_tag" >> $GITHUB_ENV

          CI_TARGET=uregressions
          docker build --no-cache -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg FSTAR_CI_BASE=$TEMP_IMAGE_NAME --build-arg CI_TARGET="$CI_TARGET" --build-arg CI_THREADS=$(nproc) . |& tee BUILDLOG
          ci_docker_status=$(docker run $ci_docker_image_tag /bin/bash -c 'cat $FSTAR_HOME/status.txt' || echo false)
          $ci_docker_status

      - name: Tag base image
        if: ${{ (success () && github.ref_name == 'master') || inputs.force }}
        run: |
          docker tag ${TEMP_IMAGE_NAME} fstar_ci_base

      - name: Compute elapsed time and status message
        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)
            if orange_contents="$(docker run $ci_docker_image_tag /bin/bash -c 'cat $FSTAR_HOME/orange_file.txt')" && [[ $orange_contents = '' ]] ; then
              echo "CI_EMOJI=✅" >> $GITHUB_ENV
            else
              echo "CI_EMOJI=⚠" >> $GITHUB_ENV
            fi
            ;;
          (cancelled)
            echo "CI_EMOJI=⚠" >> $GITHUB_ENV
            ;;
          (*)
            echo "CI_EMOJI=❌" >> $GITHUB_ENV
            ;;
          esac
          echo "CI_COMMIT=$(echo ${{ github.sha }} | grep -o '^........')" >> $GITHUB_ENV
          echo "CI_COMMIT_URL=https://github.com/FStarLang/FStar/commit/${{ github.sha }}" >> $GITHUB_ENV
          if [[ '${{github.event_name}}' == 'schedule' ]]; then
            CI_TRIGGER='schedule'
          else
            CI_TRIGGER='${{github.triggering_actor}}'
          fi
          echo "CI_TRIGGER=$CI_TRIGGER" >> $GITHUB_ENV
          echo 'CI_STATUS='"$(docker run $ci_docker_image_tag /bin/bash -c 'cat $FSTAR_HOME/result.txt' || echo Failure)" >> $GITHUB_ENV
          if [ -n "$CI_IMAGEBUILD_INITIAL_TIMESTAMP" ]; then
            DIFF=$(( $CI_IMAGEBUILD_FINAL_TIMESTAMP - $CI_IMAGEBUILD_INITIAL_TIMESTAMP ))
            SS=$(( $DIFF % 60 ))
            MM=$(( ($DIFF / 60) % 60 ))
            HH=$(( $DIFF / 3600 ))
            CI_IMAGEBUILD_TIME="${HH}h ${MM}min ${SS}s"
            echo "CI_IMAGEBUILD_TIME=$CI_IMAGEBUILD_TIME" >> $GITHUB_ENV
          fi

      - name: Remove intermediate images
        if: ${{ always() }}
        run: |
          docker rmi -f ${TEMP_IMAGE_NAME} || true
          docker rmi -f ${ci_docker_image_tag} || true

      - 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
          grep -C10 -E ' \*\*\* |\(Error' BUILDLOG > BUILDLOG_ERRORS || true
          ERRORS_URL=$(.scripts/sprang BUILDLOG_ERRORS)
          ERRORS_MSG=" <$ERRORS_URL|(Error summary)>"
          echo "ERRORS_MSG=$ERRORS_MSG" >> $GITHUB_ENV

      - name: Post to the Slack channel
        if: ${{ always() }}
        id: slack
        uses: slackapi/slack-github-action@v1.23.0
        with:
          channel-id: ${{ env.CI_SLACK_CHANNEL }}
          payload: |
            {
              "blocks" : [
                {
                  "type": "section",
                  "text": {
                    "type": "mrkdwn",
                    "text": "Update F* base CI image\n<${{ env.CI_COMMIT_URL }}|${{ env.CI_COMMIT }}> on (${{ github.ref_name }}) by ${{ env.CI_TRIGGER }}"
                  }
                },
                {
                  "type": "section",
                  "text": {
                    "type": "mrkdwn",
                    "text": "${{ env.CI_EMOJI }} <https://github.com/${{github.repository}}/actions/runs/${{github.run_id}}|${{ env.CI_STATUS }}>${{env.ERRORS_MSG}}"
                  }
                },
                {
                  "type": "section",
                  "text": {
                    "type": "plain_text",
                    "text": "Duration (image build): ${{ env.CI_IMAGEBUILD_TIME }}\nDuration (FStar CI): ${{ 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