Rebuild base image #580
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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@v4 | |
| - 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 | |
| docker build --no-cache -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg FSTAR_CI_BASE=$TEMP_IMAGE_NAME --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 | |
| continue-on-error: true | |
| uses: slackapi/[email protected] | |
| 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 |