From fc4c15ebd93229a8a590b99345a0c6ff5529e5eb Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Wed, 18 Sep 2024 09:15:00 +0200
Subject: [PATCH] chore: add nightly testing script to CI (#47)

---
 .github/NIGHTLY_FAILURE.md    | 11 ++++++
 .github/workflows/nightly.yml | 63 +++++++++++++++++++++++++++++++++++
 2 files changed, 74 insertions(+)
 create mode 100644 .github/NIGHTLY_FAILURE.md
 create mode 100644 .github/workflows/nightly.yml

diff --git a/.github/NIGHTLY_FAILURE.md b/.github/NIGHTLY_FAILURE.md
new file mode 100644
index 0000000..5c180ef
--- /dev/null
+++ b/.github/NIGHTLY_FAILURE.md
@@ -0,0 +1,11 @@
+---
+title: Builds failing with Lean nightly
+---
+
+The build is failing with the latest Lean nightly as of {{ date | date('YYYY-MM-DD') }}.
+
+Details:
+
+ * SubVerso ref: `{{ payload.ref }}`
+ * SubVerso SHA: `{{ payload.sha }}`
+ * Release tag: `{{ env.RELEASE_TAG }}` 
diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml
new file mode 100644
index 0000000..315b33b
--- /dev/null
+++ b/.github/workflows/nightly.yml
@@ -0,0 +1,63 @@
+name: Test with Lean nightly
+
+on:
+  workflow_dispatch:
+  schedule:
+    - cron: '0 0 * * *'  # Run every day at midnight
+
+jobs:
+  update-toolchain:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Install elan
+      run: |
+        set -o pipefail
+        ${{ matrix.platform.installer }}
+        echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+    - name: Check out code
+      uses: actions/checkout@v4
+
+    - name: Get latest release tag from leanprover/lean4-nightly
+      id: get-latest-release
+      run: |
+        RELEASE_TAG="$(curl -s "https://api.github.com/repos/leanprover/lean4-nightly/releases" | jq -r '.[0].tag_name')"
+        echo "RELEASE_TAG=$RELEASE_TAG" >> "${GITHUB_ENV}"
+
+    - name: Select Lean version ${{env.RELEASE_TAG}}
+      run: |
+        echo "leanprover/lean4:${RELEASE_TAG}" > lean-toolchain
+
+    - name: Build the project
+      continue-on-error: true
+      id: build
+      run: |
+        lake build
+
+    - name: Configure demo/test subproject
+      if: always() && steps.build.outcome == 'success'
+      continue-on-error: true
+      id: config-test
+      run: |
+        pushd demo
+        lake update
+        lake build :examples
+        popd
+
+    - name: Run tests
+      if: always() && steps.config-test.outcome == 'success'
+      continue-on-error: true
+      id: test
+      run: |
+        lake exe subverso-tests
+
+    - name: Create/update issue on failure
+      if: always() && (steps.build.outcome == 'failure') || (steps.config-test.outcome == 'failure') || (steps.test.outcome == 'failure')
+      uses: JasonEtco/create-an-issue@v2
+      env:
+        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      with:
+        update_existing: true
+        search_existing: open
+        filename: .github/NIGHTLY_FAILURE.md