From 255b702c627ba318ebbd0a214bc6b5e50fc9d41c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 8 Jan 2025 00:03:48 -0800 Subject: [PATCH 1/2] New Github actions CI Similar to Pulse --- .github/workflows/ci.yml | 111 +++++++++++++++++++++++++++++ .github/workflows/linux-x64.yaml | 118 ------------------------------- 2 files changed, 111 insertions(+), 118 deletions(-) create mode 100644 .github/workflows/ci.yml delete mode 100644 .github/workflows/linux-x64.yaml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 000000000..d347a0a58 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,111 @@ +name: Steel CI +on: + push: + branches-ignore: + - _** + pull_request: + workflow_dispatch: + +defaults: + run: + shell: bash + +jobs: + ci: + runs-on: ubuntu-latest + container: mtzguido/dev-base + steps: + - name: Cleanup + run: sudo find . -delete + + - run: echo "HOME=/home/user" | sudo tee -a $GITHUB_ENV + - uses: mtzguido/set-opam-env@master + + - uses: actions/checkout@master + id: checkout-fstar + with: + path: FStar + repository: FStarLang/FStar + ref: master + + - name: Try fetch built F* + id: cache-fstar + uses: actions/cache/restore@v4 + with: + path: FStar + key: FStar-${{ runner.os }}-${{ runner.arch }}-${{ steps.checkout-fstar.outputs.commit }} + + - name: Build F* + if: steps.cache-fstar.outputs.cache-hit != 'true' + run: | + make -C FStar ADMIT=1 -sj$(nproc) + + - name: Save built F* + if: steps.cache-fstar.outputs.cache-hit != 'true' + uses: actions/cache/save@v4 + with: + path: FStar + key: FStar-${{ runner.os }}-${{ runner.arch }}-${{ steps.checkout-fstar.outputs.commit }} + + - run: echo "FSTAR_EXE=$(pwd)/FStar/bin/fstar.exe" | sudo tee -a $GITHUB_ENV + - run: echo "FSTAR_HOME=$(pwd)/FStar" | sudo tee -a $GITHUB_ENV + - run: echo "PATH=$(pwd)/FStar/bin:$PATH" | sudo tee -a $GITHUB_ENV + + - uses: actions/checkout@master + id: checkout-karamel + with: + path: karamel + repository: FStarLang/karamel + ref: master + + - name: Try fetch built karamel + id: cache-karamel + uses: actions/cache/restore@v4 + with: + path: karamel + key: karamel-${{ runner.os }}-${{ runner.arch }}-${{ steps.checkout-fstar.outputs.commit }}-${{ steps.checkout-karamel.outputs.commit }} + + - name: Build karamel (if not cached) + if: steps.cache-karamel.outputs.cache-hit != 'true' + run: | + make -C karamel -sj$(nproc) + + - name: Save built karamel + if: steps.cache-karamel.outputs.cache-hit != 'true' + uses: actions/cache/save@v4 + with: + path: karamel + key: karamel-${{ runner.os }}-${{ runner.arch }}-${{ steps.checkout-fstar.outputs.commit }}-${{ steps.checkout-karamel.outputs.commit }} + + - run: echo "KRML_HOME=$(pwd)/karamel" | sudo tee -a $GITHUB_ENV + + - uses: actions/checkout@master + with: + path: steel + + - name: Steel CI + id: cistep + run: make -C steel ci -skj$(nproc) + + - name: Calculate Time + if: ${{ always () }} + id: duration + uses: RockyIsHere/actions-calculate-log-time@v0.2.4 + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + + - name: Post result to Zulip + if: ${{ always () }} # && secrets.ZULIP_API_KEY != '' }} + continue-on-error: true + uses: zulip/github-actions-zulip/send-message@v1 + with: + api-key: ${{ secrets.ZULIP_API_KEY }} + email: "github-commits-bot@fstar.zulipchat.com" + organization-url: "https://fstar.zulipchat.com" + to: "steel-ci" + type: "stream" + topic: "CI on '${{github.ref_name}}'" + content: | + '${{ github.event.head_commit.message || github.event.pull_request.title || github.head_commit.message }}' by ${{ github.event.head_commit.author.username || github.event.pull_request.user.login || github.head_commit.author.username }} (commit [${{github.sha}}](${{ github.event.head_commit.url || github.even.pull_request.html_url}})) + Status: ${{ steps.cistep.outcome == 'success' && '✅' || steps.cistep.outcome == 'cancelled' && '⚠' || '❌' }} ([link](https://github.com/${{github.repository}}/actions/runs/${{github.run_id}})) + Elapsed time: ${{ steps.duration.outputs.duration }} diff --git a/.github/workflows/linux-x64.yaml b/.github/workflows/linux-x64.yaml deleted file mode 100644 index f0ae47992..000000000 --- a/.github/workflows/linux-x64.yaml +++ /dev/null @@ -1,118 +0,0 @@ -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@v4 - - 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 - # F* CI no longer generating images, avoid hierarchical build - echo 'CI_FLAVOR=ci' >> $GITHUB_ENV - - 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 - if ! { echo $GITHUB_REF_NAME | grep '/' ; } ; then - docker tag $ci_docker_image_tag steel:local-branch-$GITHUB_REF_NAME - fi - docker tag $ci_docker_image_tag steel: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.26.0 - continue-on-error: true - 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 }} ${{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 From b3670ba9cff1d724a99d007f1439057bf5e78fc7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 9 Jan 2025 10:37:15 -0800 Subject: [PATCH 2/2] ci.yml: add ciok for branch protection --- .github/workflows/ci.yml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d347a0a58..aaa0b738b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -109,3 +109,10 @@ jobs: '${{ github.event.head_commit.message || github.event.pull_request.title || github.head_commit.message }}' by ${{ github.event.head_commit.author.username || github.event.pull_request.user.login || github.head_commit.author.username }} (commit [${{github.sha}}](${{ github.event.head_commit.url || github.even.pull_request.html_url}})) Status: ${{ steps.cistep.outcome == 'success' && '✅' || steps.cistep.outcome == 'cancelled' && '⚠' || '❌' }} ([link](https://github.com/${{github.repository}}/actions/runs/${{github.run_id}})) Elapsed time: ${{ steps.duration.outputs.duration }} + + # Main is protected to require this job. + ciok: + runs-on: ubuntu-latest + needs: ci + steps: + - run: exit 0