Rework CI

.github/workflows/nightly.yml

@@ -2,9 +2,15 @@ on:
   schedule:
     - cron: '0 0 * * *'
   workflow_dispatch:
+  push:
+
+# Cancel previous versions of this job that are still running.
+concurrency:
+  group: nightly
+  cancel-in-progress: true
 
 jobs:
-  nightly:
+  update-flake:
     runs-on: [self-hosted, linux, nix]
     steps:
       - name: checkout
@@ -13,42 +19,130 @@ jobs:
       - name: update
         run: ./update.sh
 
+      # Commit the update onto a new branch
       - name: commit
         run: |
           [[ $(git diff) != "" ]] || exit 0
           git config --local user.name "Prosecco"
           git config --local user.email "[email protected]"
+          git checkout -b nightly
           git commit -am "nightly update"
+          git push origin --force nightly:nightly
+
+  # This would be nicer as a matrix, but that hits limits of what github actions can currenctly express. See e.g.:
+  # - https://github.com/orgs/community/discussions/17245
+  # - https://github.com/orgs/community/discussions/26640
+  # - https://github.com/actions/runner/pull/2477
+  hax:
+    needs: update-flake
+    runs-on: [self-hosted, linux, nix]
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+        with:
+          ref: nightly
+      # - run: nix build -L --no-link ".#hax"
+      - run: true
+
+  charon:
+    needs: update-flake
+    runs-on: [self-hosted, linux, nix]
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+        with:
+          ref: nightly
+      # - run: nix build -L --no-link ".#charon"
+      - run: true
+
+  eurydice:
+    needs: update-flake
+    runs-on: [self-hosted, linux, nix]
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+        with:
+          ref: nightly
+      # - run: nix build -L --no-link ".#eurydice"
+      - run: false
+
+  ml-kem:
+    needs: update-flake
+    runs-on: [self-hosted, linux, nix]
+    steps:
+      - name: checkout
+        with:
+          ref: nightly
+        uses: actions/checkout@v4
+      # - run: nix build -L --no-link ".#ml-kem"
+      - run: false
+
+  bertie:
+    needs: update-flake
+    runs-on: [self-hosted, linux, nix]
+    steps:
+      - name: checkout
+        with:
+          ref: nightly
+        uses: actions/checkout@v4
+      # - run: nix build -L --no-link ".#bertie"
+      - run: true
 
-      - name: push
-        uses: ad-m/github-push-action@master
+  success:
+    needs: [hax, charon, eurydice, ml-kem, bertie]
+    runs-on: [self-hosted, linux, nix]
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
         with:
-          branch: main
+          ref: nightly
+
+      - name: commit the good flake.lock
+        run: |
+          [[ $(git diff) != "" ]] || exit 0
+          git config --local user.name "Prosecco"
+          git config --local user.email "[email protected]"
+          cp flake.lock good.lock
+          git commit -am "record the last-good flake lock"
+          git push
+
+  complete:
+    needs: [hax, charon, eurydice, ml-kem, bertie, success]
+    runs-on: [self-hosted, linux, nix]
+    if: ${{ success() || failure() }} # Will always run unless canceled
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+        with:
+          ref: nightly
 
       - name: generate zulip message
+        env:
+          RUN: ${{ github.run_id }}
+          RESULTS: ${{ toJSON(needs) }}
         run: |
+          echo "$RESULT" > result.json
           {
             echo 'MSG<<EOF'
-            echo "*Nightly update*"
             nix shell nixpkgs#jq --command ./message.sh
             echo EOF
           } >> "$GITHUB_ENV"
-        env:
-          RUN: ${{ github.run_id }}
+          rm result.json
+          cat "$GITHUB_ENV"
 
-      - name: send zulip info message
-        uses: slackapi/[email protected]
-        with:
-          payload: |
-            { "text": ${{ toJSON(env.MSG) }} }
-        env:
-          SLACK_WEBHOOK_URL: ${{ secrets.ZULIP_WEBHOOK_URL }}
+      # - name: send zulip info message
+      #   uses: slackapi/[email protected]
+      #   with:
+      #     payload: |
+      #       { "text": ${{ toJSON(env.MSG) }} }
+      #   env:
+      #     SLACK_WEBHOOK_URL: ${{ secrets.ZULIP_WEBHOOK_URL }}
 
-      - name: send zulip error message
-        if: ${{ failure() }}
-        uses: slackapi/[email protected]
-        with:
-          payload: |
-            { "text": "Unexpected Error: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" }
-        env:
-          SLACK_WEBHOOK_URL: ${{ secrets.ZULIP_WEBHOOK_URL }}
+      # - name: send zulip error message
+      #   if: ${{ failure() }}
+      #   uses: slackapi/[email protected]
+      #   with:
+      #     payload: |
+      #       { "text": "Unexpected Error: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" }
+      #   env:
+      #     SLACK_WEBHOOK_URL: ${{ secrets.ZULIP_WEBHOOK_URL }}

message.sh

@@ -1,19 +1,35 @@
 #!/usr/bin/env bash
 
-cat STATUS.txt | grep '❌' > /dev/null && echo '❌❌❌' || echo '✅✅✅'
+echo "*Nightly update*"
+if [[ "$(jq -r .success.result result.json)" == "success" ]]; then
+    echo '✅✅✅'
+else
+    echo '❌❌❌'
+fi
 echo ""
+
 echo "*Links:*"
-echo "commit: https://github.com/inria-prosecco/circus-green/commit/$(git show-ref --hash refs/heads/main)"
+COMMIT="$(git rev-parse HEAD)"
+echo "commit: https://github.com/inria-prosecco/circus-green/commit/$COMMIT"
 echo "run: https://github.com/inria-prosecco/circus-green/actions/runs/$RUN"
 echo ""
+
 echo "*Statuses:*"
-cat STATUS.txt
+for project in hax charon eurydice ml-kem bertie; do
+    status="$(jq -r 'if .["'"$project"'"].result == "success" then "✅" else "❌" end' result.json)"
+    echo "$status $project (main)"
+done
 echo ""
+
 echo "*Tried to update:*"
 cat flake.lock good.lock | jq -s -r '
     map( .nodes |
          [ .fstar, .karamel, .hax, .charon, .eurydice, .libcrux, .bertie ] |
          map( .locked )
-    ) | transpose | map(select(.[0].rev != .[1].rev)) | .[] |
-    (.[0].repo + ": [" + .[1].rev[0:8] + ".." + .[0].rev[0:8] + "](https://github.com/" + .[0].owner + "/" + .[0].repo + "/compare/" + .[1].rev[0:8] + "..." + .[0].rev[0:8] + ")")
+    )
+    | transpose
+    | .[]
+    | select(.[0].rev != .[1].rev)
+    | "\(.[1].rev[0:8])..\(.[0].rev[0:8])" as $range
+    | "\(.[0].repo): [\($range)](https://github.com/\(.[0].owner)/\(.[0].repo)/compare/\($range))"
     '

update.sh

@@ -6,29 +6,10 @@ EURYDICE_BRANCH="${EURYDICE_BRANCH:-main}"
 LIBCRUX_BRANCH="${LIBCRUX_BRANCH:-main}"
 BERTIE_BRANCH="${BERTE_BRANCH:-main}"
 
-# update `flake.lock`
+# Update `flake.lock`
 nix flake update \
    --override-input hax "github:hacspec/hax?ref=$HAX_BRANCH" \
    --override-input charon "github:aeneasverif/charon?ref=$CHARON_BRANCH" \
    --override-input eurydice "github:aeneasverif/eurydice?ref=$EURYDICE_BRANCH" \
    --override-input libcrux "github:cryspen/libcrux?ref=$LIBCRUX_BRANCH" \
    --override-input bertie "github:cryspen/bertie?ref=$BERTIE_BRANCH"
-
-# update `STATUS.txt`
-check () {
-    echo "##[group]$1"
-    STATUS=$(nix build -L --no-link ".#$1" && echo ✅ || echo ❌)
-    echo "##[endgroup]"
-    echo "$STATUS $1 ($2)" >> STATUS.txt
-}
-rm -f STATUS.txt
-check "hax" "$HAX_BRANCH"
-check "charon" "$CHARON_BRANCH"
-check "eurydice" "$EURYDICE_BRANCH"
-check "ml-kem" "$LIBCRUX_BRANCH"
-check "bertie" "$BERTIE_BRANCH"
-
-if ! cat STATUS.txt | grep -q ❌
-then
-    cp flake.lock good.lock
-fi