Skip to content

Merge remote-tracking branch 'origin/master' into nik_push_namespace #2489

Merge remote-tracking branch 'origin/master' into nik_push_namespace

Merge remote-tracking branch 'origin/master' into nik_push_namespace #2489

Workflow file for this run

name: Build and test FStar
on:
push:
branches-ignore:
- _**
pull_request:
workflow_dispatch:
inputs:
ci_refresh_hints:
description: Refresh hints and advance version number
required: true
type: boolean
ci_no_karamel:
description: Disable Karamel extraction tests
required: true
type: boolean
ci_skip_image_tag:
description: Do not tag image
required: true
type: boolean
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@v3
- name: Identify the notification channel
run: |
echo "CI_SLACK_CHANNEL=$(jq -c -r '.NotificationChannel' .docker/build/config.json)" >> $GITHUB_ENV
- name: Set the refresh hints flag
if: ${{ (github.event_name == 'workflow_dispatch') && inputs.ci_refresh_hints }}
run: |
# NOTE: this causes the build to record hints
echo "CI_TARGET=uregressions-ulong" >> $GITHUB_ENV
- name: Populate no karamel arg
if: ${{ (github.event_name == 'workflow_dispatch') && inputs.ci_no_karamel }}
run: |
echo "CI_DO_NO_KARAMEL=--build-arg CI_NO_KARAMEL=1" >> $GITHUB_ENV
- name: Populate skip image tag arg
if: ${{ (github.event_name == 'workflow_dispatch') && inputs.ci_skip_image_tag }}
run: |
echo "CI_SKIP_IMAGE_TAG=1" >> $GITHUB_ENV
- name: Enable resource monitoring
if: ${{ vars.FSTAR_CI_RESOURCEMONITOR == '1' }}
run: |
echo "RESOURCEMONITOR=1" >> $GITHUB_ENV
- name: Make sure base image is present, or build it
run: |
if ! docker images | grep '^fstar_ci_base '; then
echo '*** REBUILDING fstar_ci_base image'
CI_IMAGEBUILD_INITIAL_TIMESTAMP=$(date '+%s')
docker build -f .docker/base.Dockerfile -t fstar_ci_base .
CI_IMAGEBUILD_FINAL_TIMESTAMP=$(date '+%s')
echo "CI_IMAGEBUILD_INITIAL_TIMESTAMP=$CI_IMAGEBUILD_INITIAL_TIMESTAMP" >> $GITHUB_ENV
echo "CI_IMAGEBUILD_FINAL_TIMESTAMP=$CI_IMAGEBUILD_FINAL_TIMESTAMP" >> $GITHUB_ENV
fi
- name: Build FStar and its dependencies
run: |
ci_docker_image_tag=fstar:local-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
echo "ci_docker_image_tag=$ci_docker_image_tag" >> $GITHUB_ENV
if [[ -z $CI_TARGET ]] ; then CI_TARGET=uregressions ; fi
docker build -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg CI_BRANCH=$GITHUB_REF_NAME --build-arg CI_TARGET="$CI_TARGET" --build-arg RESOURCEMONITOR=$RESOURCEMONITOR --build-arg CI_THREADS=$(nproc) $CI_DO_NO_KARAMEL . |& tee BUILDLOG
ci_docker_status=$(docker run $ci_docker_image_tag /bin/bash -c 'cat $FSTAR_HOME/status.txt' || echo false)
if $ci_docker_status && [[ -z "$CI_SKIP_IMAGE_TAG" ]] ; then
if ! { echo $GITHUB_REF_NAME | grep '/' ; } ; then
docker tag $ci_docker_image_tag fstar:local-branch-$GITHUB_REF_NAME
fi
docker tag $ci_docker_image_tag fstar:local-commit-$GITHUB_SHA
fi
$ci_docker_status
- name: Push the generated hints
if: ${{ (github.event_name == 'workflow_dispatch') && inputs.ci_refresh_hints }}
run: |
FSTAR_HOME=$(docker run $ci_docker_image_tag /bin/bash -c 'echo $FSTAR_HOME')
docker run $ci_docker_image_tag bash -c "env DZOMO_GITHUB_TOKEN=$DZOMO_GITHUB_TOKEN $FSTAR_HOME/.scripts/advance.sh refresh_fstar_hints"
env:
DZOMO_GITHUB_TOKEN: ${{ secrets.DZOMO_GITHUB_TOKEN }}
- name: Collect resource monitoring files and summary
if: ${{ always () && vars.FSTAR_CI_RESOURCEMONITOR == '1' }}
continue-on-error: true
run: |
# docker cp needs absolute path, obtain FSTAR_HOME
FSTAR_HOME=$(docker run $ci_docker_image_tag /bin/bash -c 'echo $FSTAR_HOME')
# We briefly kick up a container from the generated image, so
# we can extract files from it. No need to start it though.
temp_container=$(docker create $ci_docker_image_tag)
docker cp $temp_container:${FSTAR_HOME}/rmon/ rmon
docker rm -f $temp_container
# Also, read these bottom-line values into the environment so they
# can go into the Slack message.
FSTAR_CI_MEASURE_CPU=$(awk -F':' '/Total CPU/ { print $2 }' rmon/res_summary.txt)
FSTAR_CI_MEASURE_MEM=$(awk -F':' '/Total memory/ { print $2 }' rmon/res_summary.txt)
echo "FSTAR_CI_MEASURE_CPU=$FSTAR_CI_MEASURE_CPU" >> $GITHUB_ENV
echo "FSTAR_CI_MEASURE_MEM=$FSTAR_CI_MEASURE_MEM" >> $GITHUB_ENV
# Final goodie: upload the summary to sprunge.us and add a link in
# the Slack message for a 1-click report.
RMON_URL=$(.scripts/sprang rmon/res_summary.txt)
echo "RMON_URL=$RMON_URL" >> $GITHUB_ENV
- name: Save resource monitor summary as artifact
if: ${{ always () && vars.FSTAR_CI_RESOURCEMONITOR == '1' }}
continue-on-error: true
uses: actions/upload-artifact@v3
with:
name: Resource usage information (summary)
path: |
rmon/res_summary.txt
- name: Save resource monitor files as artifact
if: ${{ always () && vars.FSTAR_CI_RESOURCEMONITOR == '1' }}
continue-on-error: true
uses: actions/upload-artifact@v3
with:
name: Resource usage information (individual)
path: |
rmon/rmon.tgz
- name: Compute elapsed time and status message
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)
if orange_contents="$(docker run $ci_docker_image_tag /bin/bash -c 'cat $FSTAR_HOME/orange_file.txt')" && [[ $orange_contents = '' ]] ; then
echo "CI_EMOJI=✅" >> $GITHUB_ENV
else
echo "CI_EMOJI=⚠" >> $GITHUB_ENV
fi
;;
(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 || github.head_commit.id }} | grep -o '^........')" >> $GITHUB_ENV
echo 'CI_STATUS='"$(docker run $ci_docker_image_tag /bin/bash -c 'cat $FSTAR_HOME/result.txt' || echo Failure)" >> $GITHUB_ENV
if [ -n "$CI_IMAGEBUILD_INITIAL_TIMESTAMP" ]; then
DIFF=$(( $CI_IMAGEBUILD_FINAL_TIMESTAMP - $CI_IMAGEBUILD_INITIAL_TIMESTAMP ))
SS=$(( $DIFF % 60 ))
MM=$(( ($DIFF / 60) % 60 ))
HH=$(( $DIFF / 3600 ))
CI_IMAGEBUILD_MSG=" (base image rebuilt in ${HH}h ${MM}m ${SS}s)"
echo "CI_IMAGEBUILD_MSG='$CI_IMAGEBUILD_MSG'" >> $GITHUB_ENV
fi
- 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
grep -C10 -E ' \*\*\* |\(Error' BUILDLOG > BUILDLOG_ERRORS || true
ERRORS_URL=$(.scripts/sprang BUILDLOG_ERRORS)
ERRORS_MSG=" <$ERRORS_URL|(Error summary)>"
echo "ERRORS_MSG=$ERRORS_MSG" >> $GITHUB_ENV
- name: Post to the Slack channel
if: ${{ always() }}
id: slack
uses: slackapi/[email protected]
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 || github.head_commit.author.username }}"
}
},
{
"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}}|${{ env.CI_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.CI_IMAGEBUILD_MSG}}"
}
},
{
"type": "section",
"text": {
"type": "mrkdwn",
"text": "<${{env.RMON_URL}}|Resource summary>\nTotal CPU usage: ${{ env.FSTAR_CI_MEASURE_CPU }}\nTotal memory usage: ${{ env.FSTAR_CI_MEASURE_MEM }}"
}
}
]
}
env:
SLACK_WEBHOOK_URL: ${{ secrets.SLACK_WEBHOOK_URL }}
SLACK_WEBHOOK_TYPE: INCOMING_WEBHOOK