Merge pull request #3609 from FStarLang/_nik_induction_on_reflexive_t… #4279
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: Build and test FStar | |
| on: | |
| push: | |
| branches-ignore: | |
| - _** | |
| pull_request: | |
| workflow_dispatch: | |
| inputs: | |
| ci_refresh_hints: | |
| description: Refresh hints and advance version number | |
| required: true | |
| type: boolean | |
| ci_no_karamel: | |
| description: Disable Karamel extraction tests | |
| required: true | |
| type: boolean | |
| ci_skip_image_tag: | |
| description: Do not tag image | |
| 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: Record initial timestamp | |
| run: | | |
| echo "CI_INITIAL_TIMESTAMP=$(date '+%s')" >> $GITHUB_ENV | |
| - name: Check out repo | |
| uses: actions/checkout@v4 | |
| - name: Identify the notification channel | |
| run: | | |
| echo "CI_SLACK_CHANNEL=$(jq -c -r '.NotificationChannel' .docker/build/config.json)" >> $GITHUB_ENV | |
| - name: Set the refresh hints flag | |
| if: ${{ (github.event_name == 'workflow_dispatch') && inputs.ci_refresh_hints }} | |
| run: | | |
| # NOTE: this causes the build to record hints | |
| echo "CI_RECORD_HINTS_ARG=--build-arg CI_RECORD_HINTS=1" >> $GITHUB_ENV | |
| - name: Populate no karamel arg | |
| if: ${{ (github.event_name == 'workflow_dispatch') && inputs.ci_no_karamel }} | |
| run: | | |
| echo "CI_DO_NO_KARAMEL=--build-arg CI_NO_KARAMEL=1" >> $GITHUB_ENV | |
| - name: Populate skip image tag arg | |
| if: ${{ (github.event_name == 'workflow_dispatch') && inputs.ci_skip_image_tag }} | |
| run: | | |
| echo "CI_SKIP_IMAGE_TAG=1" >> $GITHUB_ENV | |
| - name: Enable resource monitoring | |
| if: ${{ vars.FSTAR_CI_RESOURCEMONITOR == '1' }} | |
| run: | | |
| echo "RESOURCEMONITOR=1" >> $GITHUB_ENV | |
| - name: Make sure base image is present, or build it | |
| run: | | |
| if ! docker images | grep '^fstar_ci_base '; then | |
| echo '*** REBUILDING fstar_ci_base image' | |
| CI_IMAGEBUILD_INITIAL_TIMESTAMP=$(date '+%s') | |
| docker build -f .docker/base.Dockerfile -t fstar_ci_base . | |
| 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 | |
| fi | |
| - name: Build FStar and its dependencies | |
| run: | | |
| ci_docker_image_tag=fstar:local-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT | |
| echo "ci_docker_image_tag=$ci_docker_image_tag" >> $GITHUB_ENV | |
| docker build -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg CI_BRANCH=$GITHUB_REF_NAME --build-arg RESOURCEMONITOR=$RESOURCEMONITOR --build-arg CI_THREADS=$(nproc) $CI_RECORD_HINTS_ARG $CI_DO_NO_KARAMEL . |& tee BUILDLOG | |
| ci_docker_status=$(docker run $ci_docker_image_tag /bin/bash -c 'cat $FSTAR_HOME/status.txt' || echo false) | |
| if $ci_docker_status && [[ -z "$CI_SKIP_IMAGE_TAG" ]] ; then | |
| if ! { echo $GITHUB_REF_NAME | grep '/' ; } ; then | |
| docker tag $ci_docker_image_tag fstar:local-branch-$GITHUB_REF_NAME | |
| fi | |
| docker tag $ci_docker_image_tag fstar:local-commit-$GITHUB_SHA | |
| fi | |
| $ci_docker_status | |
| - name: Push the generated hints | |
| if: ${{ (github.event_name == 'workflow_dispatch') && inputs.ci_refresh_hints }} | |
| run: | | |
| FSTAR_HOME=$(docker run $ci_docker_image_tag /bin/bash -c 'echo $FSTAR_HOME') | |
| docker run $ci_docker_image_tag bash -c "env DZOMO_GITHUB_TOKEN=$DZOMO_GITHUB_TOKEN $FSTAR_HOME/.scripts/advance.sh refresh_fstar_hints" | |
| env: | |
| DZOMO_GITHUB_TOKEN: ${{ secrets.DZOMO_GITHUB_TOKEN }} | |
| - name: Collect resource monitoring files and summary | |
| if: ${{ always () && vars.FSTAR_CI_RESOURCEMONITOR == '1' }} | |
| continue-on-error: true | |
| run: | | |
| # docker cp needs absolute path, obtain FSTAR_HOME | |
| FSTAR_HOME=$(docker run $ci_docker_image_tag /bin/bash -c 'echo $FSTAR_HOME') | |
| # We briefly kick up a container from the generated image, so | |
| # we can extract files from it. No need to start it though. | |
| temp_container=$(docker create $ci_docker_image_tag) | |
| docker cp $temp_container:${FSTAR_HOME}/rmon/ rmon | |
| docker rm -f $temp_container | |
| # Also, read these bottom-line values into the environment so they | |
| # can go into the Slack message. | |
| FSTAR_CI_MEASURE_CPU=$(awk -F':' '/Total CPU/ { print $2 }' rmon/res_summary.txt) | |
| FSTAR_CI_MEASURE_MEM=$(awk -F':' '/Total memory/ { print $2 }' rmon/res_summary.txt) | |
| echo "FSTAR_CI_MEASURE_CPU=$FSTAR_CI_MEASURE_CPU" >> $GITHUB_ENV | |
| echo "FSTAR_CI_MEASURE_MEM=$FSTAR_CI_MEASURE_MEM" >> $GITHUB_ENV | |
| # Final goodie: upload the summary to sprunge.us and add a link in | |
| # the Slack message for a 1-click report. | |
| RMON_URL=$(.scripts/sprang rmon/res_summary.txt) | |
| echo "RMON_URL=$RMON_URL" >> $GITHUB_ENV | |
| - name: Save resource monitor summary as artifact | |
| if: ${{ always () && vars.FSTAR_CI_RESOURCEMONITOR == '1' }} | |
| continue-on-error: true | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: Resource usage information (summary) | |
| path: | | |
| rmon/res_summary.txt | |
| - name: Save resource monitor files as artifact | |
| if: ${{ always () && vars.FSTAR_CI_RESOURCEMONITOR == '1' }} | |
| continue-on-error: true | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: Resource usage information (individual) | |
| path: | | |
| rmon/rmon.tgz | |
| - 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.event.head_commit.id || github.event.pull_request.head.sha || github.head_commit.id }} | grep -o '^........')" >> $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_MSG=" (base image rebuilt in ${HH}h ${MM}m ${SS}s)" | |
| echo "CI_IMAGEBUILD_MSG='$CI_IMAGEBUILD_MSG'" >> $GITHUB_ENV | |
| fi | |
| - 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": "<${{ 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 || github.head_commit.author.username }}" | |
| } | |
| }, | |
| { | |
| "type": "section", | |
| "text": { | |
| "type": "plain_text", | |
| "text": ${{ toJSON(github.event.head_commit.message || github.event.pull_request.title || github.head_commit.message || '<unknown>') }} | |
| } | |
| }, | |
| { | |
| "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: ${{ env.CI_TIME_DIFF_H }}h ${{ env.CI_TIME_DIFF_M }}min ${{ env.CI_TIME_DIFF_S }}s${{env.CI_IMAGEBUILD_MSG}}" | |
| } | |
| }, | |
| { | |
| "type": "section", | |
| "text": { | |
| "type": "mrkdwn", | |
| "text": "<${{env.RMON_URL}}|Resource summary>\nTotal CPU usage: ${{ env.FSTAR_CI_MEASURE_CPU }}\nTotal memory usage: ${{ env.FSTAR_CI_MEASURE_MEM }}" | |
| } | |
| } | |
| ] | |
| } | |
| env: | |
| SLACK_WEBHOOK_URL: ${{ secrets.SLACK_WEBHOOK_URL }} | |
| SLACK_WEBHOOK_TYPE: INCOMING_WEBHOOK |