pulse ht: pulse insert,delete,lookup loop invariants check with new p… #543
Workflow file for this run
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 Steel | |
| 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 Steel and its dependencies | |
| run: | | |
| ci_docker_image_tag=steel: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 . |& tee BUILDLOG | |
| - 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 | |
| if grep -C10 -E ' \*\*\* |\(Error' BUILDLOG > BUILDLOG_ERRORS; then | |
| 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 |