From 831fa828f66cd3aa07bf14d3f471e9105499268b Mon Sep 17 00:00:00 2001
From: Oscar M <143578027+Oscario0@users.noreply.github.com>
Date: Tue, 6 Jan 2026 14:33:23 -0500
Subject: [PATCH 1/2] bumps lean version to latest release

---
 .github/workflows/update-lean-version.yml | 79 +++++++++++++++++++++++
 1 file changed, 79 insertions(+)
 create mode 100644 .github/workflows/update-lean-version.yml

diff --git a/.github/workflows/update-lean-version.yml b/.github/workflows/update-lean-version.yml
new file mode 100644
index 0000000..5cc073f
--- /dev/null
+++ b/.github/workflows/update-lean-version.yml
@@ -0,0 +1,79 @@
+name: Update Lean Version
+
+on:
+  schedule:
+    # Runs every night at 2 AM UTC
+    - cron: "0 2 * * *"
+  workflow_dispatch: # for manual trigger
+
+jobs:
+  update-lean:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Get current Lean version
+        id: current
+        run: |
+          CURRENT_VERSION=$(cat lean-toolchain | tr -d '[:space:]')
+          echo "version=$CURRENT_VERSION" >> $GITHUB_OUTPUT
+          echo "Current version: $CURRENT_VERSION"
+
+      - name: Get latest Lean 4 stable version
+        id: latest
+        run: |
+          LATEST=$(curl -s https://api.github.com/repos/leanprover/lean4/releases | \
+            jq -r '[.[] | select(.prerelease == false and (.tag_name | test("^v[0-9]+\\.[0-9]+\\.[0-9]+$")))][0].tag_name')
+          echo "version=leanprover/lean4:$LATEST" >> $GITHUB_OUTPUT
+          echo "Latest stable version: leanprover/lean4:$LATEST"
+
+      - name: Check if update needed
+        id: check
+        run: |
+          if [ "${{ steps.current.outputs.version }}" != "${{ steps.latest.outputs.version }}" ]; then
+            echo "update_needed=true" >> $GITHUB_OUTPUT
+            echo "Update needed: ${{ steps.current.outputs.version }} -> ${{ steps.latest.outputs.version }}"
+          else
+            echo "update_needed=false" >> $GITHUB_OUTPUT
+            echo "Already on latest version"
+          fi
+
+      - name: Update lean-toolchain
+        if: steps.check.outputs.update_needed == 'true'
+        run: |
+          echo "${{ steps.latest.outputs.version }}" > lean-toolchain
+          cat lean-toolchain
+
+      - name: Install elan
+        if: steps.check.outputs.update_needed == 'true'
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Update dependencies
+        if: steps.check.outputs.update_needed == 'true'
+        id: deps
+        run: |
+          export PATH="$HOME/.elan/bin:$PATH"
+          # Update all dependencies to latest compatible versions
+          lake update 2>&1 | tee update.log
+          echo "deps_updated=true" >> $GITHUB_OUTPUT
+
+      - name: Test build
+        if: steps.check.outputs.update_needed == 'true'
+        id: build
+        continue-on-error: true
+        run: |
+          export PATH="$HOME/.elan/bin:$PATH"
+          lake build 2>&1 | tee build.log
+          if [ $? -eq 0 ]; then
+            echo "build_status=success" >> $GITHUB_OUTPUT
+          else
+            echo "build_status=failed" >> $GITHUB_OUTPUT
+          fi

From d6e51206083a613bf90ef1463e7169b798d0abf0 Mon Sep 17 00:00:00 2001
From: Oscar M <143578027+Oscario0@users.noreply.github.com>
Date: Wed, 21 Jan 2026 20:33:30 -0500
Subject: [PATCH 2/2] bumps lean version to latest release (#1)

---
 .github/workflows/update-lean-version.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/update-lean-version.yml b/.github/workflows/update-lean-version.yml
index 5cc073f..d598a4d 100644
--- a/.github/workflows/update-lean-version.yml
+++ b/.github/workflows/update-lean-version.yml
@@ -72,7 +72,8 @@ jobs:
         run: |
           export PATH="$HOME/.elan/bin:$PATH"
           lake build 2>&1 | tee build.log
-          if [ $? -eq 0 ]; then
+          build_exit_code=${PIPESTATUS[0]}
+          if [ "$build_exit_code" -eq 0 ]; then
             echo "build_status=success" >> $GITHUB_OUTPUT
           else
             echo "build_status=failed" >> $GITHUB_OUTPUT