Merge pull request #290 from FStarLang/_taramana_slice_to_from_array_ptr #1010
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 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 |