From b11134b652bd1e238d9740e0bcff43c58426f38c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Tue, 7 Jan 2025 17:02:19 -0800
Subject: [PATCH 1/3] book/conf.py: set language to english

Avoids a warning, which is treated as an error on some Sphinx versions.
---
 book/conf.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/book/conf.py b/book/conf.py
index b35007a7c..3d094204f 100644
--- a/book/conf.py
+++ b/book/conf.py
@@ -60,7 +60,7 @@
 #
 # This is also used if you do content translation via gettext catalogs.
 # Usually you set "language" from the command line for these cases.
-language = None
+language = 'english'
 
 # List of patterns, relative to source directory, that match files and
 # directories to ignore when looking for source files.

From 45b3c002df6ee8e1d97fad888e799a85f584c29a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Mon, 30 Dec 2024 10:15:00 -0800
Subject: [PATCH 2/3] Github actions CI

This changes the CI to be completely cloud hosted and independent of the
runner machine. I think all features are retained and the .docker
directory can be blasted away.

Note that soon the buildmachine will stop building F* images, so the old
workflow will go through the 'standalone' path and be slower.
---
 .github/workflows/ci.yml                    | 135 +++++++++++++++++++
 .github/workflows/linux-x64-hierarchic.yaml | 138 --------------------
 .scripts/publish_tutorial.sh                |  27 ++++
 3 files changed, 162 insertions(+), 138 deletions(-)
 create mode 100644 .github/workflows/ci.yml
 delete mode 100644 .github/workflows/linux-x64-hierarchic.yaml
 create mode 100755 .scripts/publish_tutorial.sh

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 000000000..2ca162b78
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,135 @@
+name: CI
+on:
+  push:
+    branches-ignore:
+    - _**
+  pull_request:
+  workflow_dispatch:
+  schedule:
+    - cron: '0 0 * * *'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  build-and-test:
+    runs-on: ubuntu-latest
+    container: mtzguido/dev-base
+    steps:
+      - run: echo "HOME=/home/user" >> $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 -skj$(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" >> $GITHUB_ENV
+      - run: echo "FSTAR_HOME=$(pwd)/FStar" >> $GITHUB_ENV
+      - run: echo "PATH=$(pwd)/FStar/bin:$PATH" >> $GITHUB_ENV
+
+      - uses: actions/checkout@master
+        with:
+          path: karamel
+
+      - uses: actions/setup-node@v4
+        with:
+          node-version: 16
+
+      - run: echo "KRML_HOME=$(pwd)/karamel" >> $GITHUB_ENV
+
+      - name: Karamel CI
+        working-directory: karamel
+        run: |
+          . $HOME/.cargo/env
+          export OCAMLRUNPARAM=b
+          make -kj$(nproc)
+          make -kj$(nproc) -C test everything
+
+      - name: Build book
+        working-directory: karamel
+        run: |
+          sudo apt-get install -y python3-sphinx python3-sphinx-rtd-theme
+          make -C book html
+
+      - name: Upload book artifact
+        uses: actions/upload-artifact@v4
+        with:
+          path: karamel/book/_build
+          name: book
+
+  # This is checked in parallel with no F* around. It checks that the
+  # krllib snapshot builds, on several systems.
+  build-krmllib:
+    strategy:
+      matrix:
+        os:
+          - ubuntu-20.04
+          - ubuntu-22.04
+          - ubuntu-24.04
+          - macos-13
+          - macos-14
+          - macos-15
+        cc:
+          - gcc
+          - clang
+
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: actions/checkout@master
+      - name: Build the checked-in krmllib
+        run: |
+          export KRML_HOME=$(pwd)
+          export CC=${{matrix.cc}}
+          make -kj$(nproc) -C krmllib/dist/generic -f Makefile.basic
+
+  # A single no-op job to use for branch protection
+  ciok:
+    runs-on: ubuntu-latest
+    needs:
+      - build-and-test
+      - build-krmllib
+    steps:
+      - run: true
+
+  publish_book:
+    runs-on: ubuntu-latest
+    if: ${{ github.ref == 'refs/heads/master' }}
+    needs: build-and-test
+    steps:
+      - uses: actions/checkout@master
+      - uses: actions/download-artifact@v4
+        with:
+          name: book
+          path: book/_build
+
+      - name: Configure git
+        run: |
+          git config --global user.name "Dzomo, the Everest Yak"
+          git config --global user.email "24394600+dzomo@users.noreply.github.com"
+
+      - run: .scripts/publish_tutorial.sh
+        env:
+          DZOMO_GITHUB_TOKEN: ${{secrets.DZOMO_GITHUB_TOKEN}}
diff --git a/.github/workflows/linux-x64-hierarchic.yaml b/.github/workflows/linux-x64-hierarchic.yaml
deleted file mode 100644
index 47785c74c..000000000
--- a/.github/workflows/linux-x64-hierarchic.yaml
+++ /dev/null
@@ -1,138 +0,0 @@
-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
diff --git a/.scripts/publish_tutorial.sh b/.scripts/publish_tutorial.sh
new file mode 100755
index 000000000..38e44aaf2
--- /dev/null
+++ b/.scripts/publish_tutorial.sh
@@ -0,0 +1,27 @@
+#!/bin/bash
+
+set -eux
+
+# Run from the root of the repo, with a built book, and DZOMO_GITHUB_TOKEN set
+# in the environment. This is called by ci.yml on every push to master.
+
+git clone "https://$DZOMO_GITHUB_TOKEN@github.com/fstarlang/fstarlang.github.io"
+
+pushd fstarlang.github.io
+
+cp -R ../book/_build/* lowstar/
+rm -rf lowstar/html/static
+mv lowstar/html/_static lowstar/html/static
+find lowstar/html -type f | xargs sed -i 's/_static/static/g'
+git add -A lowstar/html lowstar/index.html
+
+git status
+
+if ! git diff --exit-code HEAD > /dev/null; then
+  git commit -m '[CI] Refresh Low* tutorial'
+  git push
+else
+  echo "No git diff for the tutorial"
+fi
+
+exit 0

From d4ab372be23c8ef34e9c97dec3990fb4674400ad Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 8 Jan 2025 19:53:26 -0800
Subject: [PATCH 3/3] README: update CI badge

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 589981903..3c0396bb7 100644
--- a/README.md
+++ b/README.md
@@ -3,7 +3,7 @@ KaRaMeL
 
 | Linux  |
 |---------|
-| [![Build and Deploy](https://github.com/FStarLang/karamel/actions/workflows/linux-x64-hierarchic.yaml/badge.svg)](https://github.com/FStarLang/karamel/actions/workflows/linux-x64-hierarchic.yaml) |
+[![CI](https://github.com/FStarLang/karamel/actions/workflows/ci.yml/badge.svg)](https://github.com/FStarLang/karamel/actions/workflows/ci.yml)
 
 KaRaMeL (formerly known as KReMLin) is a tool that extracts an F\* program to
 readable C code: K&R meets ML!