From c644ddf887d59813d8a11e63a4df2c801db4194b Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Wed, 29 Mar 2023 11:03:33 -0700
Subject: [PATCH] add Steel CI with FStarLang/FStar#2349

---
 .docker/steel.Dockerfile     | 25 ++++++++++
 .github/workflows/steel.yaml | 92 ++++++++++++++++++++++++++++++++++++
 2 files changed, 117 insertions(+)
 create mode 100644 .docker/steel.Dockerfile
 create mode 100644 .github/workflows/steel.yaml

diff --git a/.docker/steel.Dockerfile b/.docker/steel.Dockerfile
new file mode 100644
index 000000000..96d0580f1
--- /dev/null
+++ b/.docker/steel.Dockerfile
@@ -0,0 +1,25 @@
+# This Dockerfile should be run from the root EverParse directory
+
+ARG ocaml_version=4.12
+FROM ocaml/opam:ubuntu-ocaml-$ocaml_version
+
+ADD --chown=opam:opam ./ $HOME/everparse/
+WORKDIR $HOME/everparse
+
+# CI dependencies: jq (to identify F* branch)
+RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends jq
+
+# Dependencies (F*, Karamel and opam packages)
+ENV FSTAR_HOME=$HOME/FStar
+ENV KRML_HOME=$HOME/karamel
+ENV FSTAR_BRANCH=john_ml_steel_c
+RUN eval $(opam env) && .docker/build/install-deps.sh
+
+# CI proper
+ARG CI_THREADS=24
+
+ENV STEEL_C=1
+RUN eval $(opam env) && make -j $CI_THREADS steel-unit-test
+
+WORKDIR $HOME
+ENV EVERPARSE_HOME=$HOME/everparse
diff --git a/.github/workflows/steel.yaml b/.github/workflows/steel.yaml
new file mode 100644
index 000000000..c1e3cfe83
--- /dev/null
+++ b/.github/workflows/steel.yaml
@@ -0,0 +1,92 @@
+name: Build and test EverParse+Steel
+on:
+  push:
+    branches-ignore:
+    - _**
+    - taramana_steel
+  pull_request:
+  workflow_dispatch:
+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@v2
+      - name: Identify the base FStar branch and the notification channel
+        run: |
+          echo "FSTAR_BRANCH=john_ml_steel_c" >> $GITHUB_ENV
+          echo "CI_SLACK_CHANNEL=$(jq -c -r '.NotificationChannel' .docker/build/config.json)" >> $GITHUB_ENV
+      - name: Build Everparse and its dependencies
+        run: |
+          ci_docker_image_tag=everparse:local-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
+          ci_docker_builder=builder_everparse_${GITHUB_RUN_ID}_${GITHUB_RUN_ATTEMPT}
+          docker buildx create --name $ci_docker_builder --driver-opt env.BUILDKIT_STEP_LOG_MAX_SIZE=500000000
+          docker buildx build --builder $ci_docker_builder --pull --load -t $ci_docker_image_tag -f .docker/steel.Dockerfile .
+          docker buildx rm -f $ci_docker_builder
+        env:
+          DZOMO_GITHUB_TOKEN: ${{ secrets.DZOMO_GITHUB_TOKEN }}
+      - 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: 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) }}
+                  }
+                },
+                {
+                  "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