Skip to content

Build and test Karamel based on a FStar image #1708

Build and test Karamel based on a FStar image

Build and test Karamel based on a FStar image #1708

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/slack-github-action@v1.23.0
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/slack-github-action@v1.23.0
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