Move MiniRust simplifications to OptimizeMiniRust #1603
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 Karamel based on a FStar image | |
| on: | |
| push: | |
| branches-ignore: | |
| - _** | |
| pull_request: | |
| workflow_dispatch: | |
| schedule: | |
| # Midnight UTC | |
| - cron: '0 0 * * *' | |
| jobs: | |
| build: | |
| runs-on: [self-hosted, linux, X64] | |
| steps: | |
| - name: Record initial timestamp | |
| run: | | |
| echo "CI_INITIAL_TIMESTAMP=$(date '+%s')" >> $GITHUB_ENV | |
| - name: Check out repo | |
| uses: actions/checkout@v3 | |
| - name: Identify the base FStar branch and the notification channel | |
| run: | | |
| echo "FSTAR_BRANCH=$(jq -c -r '.BranchName' .docker/build/config.json)" >> $GITHUB_ENV | |
| echo "CI_SLACK_CHANNEL=$(jq -c -r '.NotificationChannel' .docker/build/config.json)" >> $GITHUB_ENV | |
| - name: Determine the build flavor | |
| run: | | |
| if docker image inspect fstar:local-branch-$FSTAR_BRANCH ; then echo KRML_CI_FLAVOR=hierarchic >> $GITHUB_ENV ; else echo KRML_CI_FLAVOR=standalone >> $GITHUB_ENV ; fi | |
| - name: Build Karamel and its dependencies | |
| run: | | |
| ci_docker_image_tag=karamel:local-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT | |
| docker buildx build --secret id=DZOMO_GITHUB_TOKEN -t $ci_docker_image_tag -f .docker/$KRML_CI_FLAVOR.Dockerfile --build-arg FSTAR_BRANCH=$FSTAR_BRANCH --build-arg CI_BRANCH=$GITHUB_REF_NAME . | |
| if docker run $ci_docker_image_tag /bin/bash -c 'cat $KRML_HOME/result.txt' | grep Success ; then ci_docker_status=true ; else ci_docker_status=false ; fi | |
| if $ci_docker_status ; then | |
| if ! { echo $GITHUB_REF_NAME | grep '/' ; } ; then | |
| docker tag $ci_docker_image_tag karamel:local-branch-$GITHUB_REF_NAME | |
| fi | |
| docker tag $ci_docker_image_tag karamel:local-commit-$GITHUB_SHA | |
| fi | |
| docker run $ci_docker_image_tag /bin/bash -c 'cat $KRML_HOME/log.txt' > log.txt | |
| $ci_docker_status | |
| env: | |
| DZOMO_GITHUB_TOKEN: ${{ secrets.DZOMO_GITHUB_TOKEN }} | |
| - name: Archive build log | |
| if: ${{ always() }} | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: log | |
| path: log.txt | |
| - 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.sha }} | grep -o '^........')" >> $GITHUB_ENV | |
| echo "CI_COMMIT_URL=https://github.com/FStarLang/karamel/commit/${{ github.sha }}" >> $GITHUB_ENV | |
| - name: Post to the Slack channel (if push/PR) | |
| if: ${{ always() && github.event_name != 'schedule' }} | |
| id: slack-pushpr | |
| uses: slackapi/[email protected] | |
| with: | |
| channel-id: ${{ env.CI_SLACK_CHANNEL }} | |
| payload: | | |
| { | |
| "blocks" : [ | |
| { | |
| "type": "section", | |
| "text": { | |
| "type": "mrkdwn", | |
| "text": "<${{ env.CI_COMMIT_URL }}|${{ env.CI_COMMIT }}> on (${{ github.ref_name }}) by ${{github.triggering_actor}}" | |
| } | |
| }, | |
| { | |
| "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}}|${{ job.status }}>" | |
| } | |
| }, | |
| { | |
| "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 | |
| - name: Post to the Slack channel (if schedule) | |
| if: ${{ always() && github.event_name == 'schedule' }} | |
| id: slack-scheduled | |
| uses: slackapi/[email protected] | |
| with: | |
| channel-id: ${{ env.CI_SLACK_CHANNEL }} | |
| payload: | | |
| { | |
| "blocks" : [ | |
| { | |
| "type": "section", | |
| "text": { | |
| "type": "mrkdwn", | |
| "text": "${{ env.CI_EMOJI }} Nightly CI <https://github.com/${{github.repository}}/actions/runs/${{github.run_id}}|${{ job.status }}> on <${{ env.CI_COMMIT_URL }}|${{ env.CI_COMMIT }}>" | |
| } | |
| }, | |
| { | |
| "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 |