From 72c15f39163c8bff852d480581b5c11518ec9489 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Mon, 22 Sep 2025 15:04:38 +0100
Subject: [PATCH 01/30] feat: Blase evaluation via Namespace

We will use `snakemake`'s kubernetes executor:
https://snakemake.github.io/snakemake-plugin-catalog/plugins/executor/kubernetes.html

along with namespace's kubernetes cluster support:
- https://namespace.so/docs/reference/github-actions/nscloud-cluster-action

to run our snakemake setup directly on snakemake.
The open question for me is where this will store the build artifact.
Currently, our evaluation run uploads a ZIP file to Zulip.
We can upload this ZIP file as a build artifact on GH.
---
 .../evaluation-multi-width-namespace.yml      | 35 +++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 .github/workflows/evaluation-multi-width-namespace.yml

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
new file mode 100644
index 0000000000..30c292840f
--- /dev/null
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -0,0 +1,35 @@
+name: Evaluation Multi-Width (Namespace) 
+on:
+  push:
+    branches:
+      - "main"
+  pull_request:
+
+permissions:
+  contents: write
+  id-token: write
+
+jobs:
+  build:
+    name: Build & Eval Blase on NS
+    runs-on:
+      - nscloud-ubuntu-24.04-amd64-16x32-with-cache
+      - nscloud-cache-tag-my-custom-cache
+      - nscloud-cache-size-100gb
+      - nscloud-git-mirror-5gb
+      - nscloud-container-image-cache
+      - nscloud-runner-tool-cache-20gb
+
+    steps:
+      - name: Setup Ephemeral NS Cluster
+        uses: namespacelabs/nscloud-setup@v0
+
+      # https://namespace.so/docs/reference/github-actions/nscloud-checkout-action
+      - name: Checkout Evaluation Repisitory via NS
+        uses: namespacelabs/nscloud-checkout@v7
+        with:
+          repository: "github.com/opencompl/evaluation-multi-width-bv"
+          ref: "main"
+          token: ${{ secrets.NSCLOUD_GITHUB_TOKEN }}
+
+        

From 18860692efa32ea497d77db546d75f1321bf0b96 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 24 Sep 2025 08:34:34 +0100
Subject: [PATCH 02/30] chore: change checkout action to be the correct
 namespace action

---
 .github/workflows/evaluation-multi-width-namespace.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index 30c292840f..df854f5b89 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -1,4 +1,4 @@
-name: Evaluation Multi-Width (Namespace) 
+name: Evaluation Multi-Width (Namespace)
 on:
   push:
     branches:
@@ -26,10 +26,10 @@ jobs:
 
       # https://namespace.so/docs/reference/github-actions/nscloud-checkout-action
       - name: Checkout Evaluation Repisitory via NS
-        uses: namespacelabs/nscloud-checkout@v7
+        uses: namespacelabs/nscloud-checkout-action@v7
         with:
           repository: "github.com/opencompl/evaluation-multi-width-bv"
           ref: "main"
           token: ${{ secrets.NSCLOUD_GITHUB_TOKEN }}
 
-        
+

From 4cd53126453c6113eaabab58b49e0a90669f1249 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 24 Sep 2025 08:35:57 +0100
Subject: [PATCH 03/30] chore: fix URL

---
 .github/workflows/evaluation-multi-width-namespace.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index df854f5b89..c31ba5ba56 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -28,7 +28,7 @@ jobs:
       - name: Checkout Evaluation Repisitory via NS
         uses: namespacelabs/nscloud-checkout-action@v7
         with:
-          repository: "github.com/opencompl/evaluation-multi-width-bv"
+          repository: "opencompl/evaluation-multi-width-bv"
           ref: "main"
           token: ${{ secrets.NSCLOUD_GITHUB_TOKEN }}
 

From 273f10499a23b7824b9502bcc4041ca00c7db148 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 24 Sep 2025 08:38:58 +0100
Subject: [PATCH 04/30] chore; target master

---
 .github/workflows/evaluation-multi-width-namespace.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index c31ba5ba56..446792fb25 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -29,7 +29,7 @@ jobs:
         uses: namespacelabs/nscloud-checkout-action@v7
         with:
           repository: "opencompl/evaluation-multi-width-bv"
-          ref: "main"
+          ref: "master"
           token: ${{ secrets.NSCLOUD_GITHUB_TOKEN }}
 
 

From 4206abb801fac64766c48b5566c9b80eae4a422a Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 24 Sep 2025 09:20:50 +0100
Subject: [PATCH 05/30] chore: add NS evaluation running script

---
 .../evaluation-multi-width-namespace.yml      | 44 +++++++++++++++++--
 1 file changed, 41 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index 446792fb25..d8cbbb40c3 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -1,4 +1,4 @@
-name: Evaluation Multi-Width (Namespace)
+name: Evaluation Multi-Width (NS)
 on:
   push:
     branches:
@@ -10,8 +10,8 @@ permissions:
   id-token: write
 
 jobs:
-  build:
-    name: Build & Eval Blase on NS
+  warm-cache:
+    name: Warm Cache via MiniEval
     runs-on:
       - nscloud-ubuntu-24.04-amd64-16x32-with-cache
       - nscloud-cache-tag-my-custom-cache
@@ -32,4 +32,42 @@ jobs:
           ref: "master"
           token: ${{ secrets.NSCLOUD_GITHUB_TOKEN }}
 
+      - name: Run MiniEval
+        run: |
+          cd evaluation-multi-width-bv
+          cp config.tiny.yaml config.yaml
+          ./run-on-container.sh
+
+      - name: Upload Warm Cache as Artifact
+        uses: namespace-actions/upload-artifact@v1
+        with:
+          name: evaluation-multi-width-bv-cache
+          path: evaluation-multi-width-bv
+          compression-level: 9
+
+  run-full-eval:
+    needs: warm-cache
+    name: Run Full Evaluation
+    runs-on:
+      - nscloud-ubuntu-24.04-amd64-16x32-with-cache
+      - nscloud-cache-tag-my-custom-cache
+      - nscloud-cache-size-100gb
+      - nscloud-git-mirror-5gb
+      - nscloud-container-image-cache
+      - nscloud-runner-tool-cache-20gb
+    steps:
+      - name: Setup Ephemeral NS Cluster
+        uses: namespacelabs/nscloud-setup@v0
+
+      - name: Download Warm Cache Artifact
+        uses: namespace-actions/download-artifact@v1
+        with:
+          name: evaluation-multi-width-bv-cache
+          path: evaluation-multi-width-bv
+
+      - name: Run Full Evaluateion
+        run: |
+          cd evaluation-multi-width-bv
+          cp config.full.yaml config.yaml
+          ./run-on-container.sh
 

From bff05b0f8aa6dbad73d6a034660630af5fa28498 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 24 Sep 2025 09:22:16 +0100
Subject: [PATCH 06/30] chore: not sure where checkout clones stuff

---
 .github/workflows/evaluation-multi-width-namespace.yml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index d8cbbb40c3..b4995fb41a 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -34,7 +34,8 @@ jobs:
 
       - name: Run MiniEval
         run: |
-          cd evaluation-multi-width-bv
+          ls
+          # cd evaluation-multi-width-bv
           cp config.tiny.yaml config.yaml
           ./run-on-container.sh
 
@@ -42,7 +43,7 @@ jobs:
         uses: namespace-actions/upload-artifact@v1
         with:
           name: evaluation-multi-width-bv-cache
-          path: evaluation-multi-width-bv
+          path: .
           compression-level: 9
 
   run-full-eval:

From 704cfa33042892aa3fdd5c36f43dc6474ea4df7a Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 24 Sep 2025 09:35:27 +0100
Subject: [PATCH 07/30] chore: curl uv

---
 .github/workflows/evaluation-multi-width-namespace.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index b4995fb41a..b21a2f51f5 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -35,6 +35,8 @@ jobs:
       - name: Run MiniEval
         run: |
           ls
+          set -o pipefail
+          curl -LsSf https://astral.sh/uv/install.sh | sh
           # cd evaluation-multi-width-bv
           cp config.tiny.yaml config.yaml
           ./run-on-container.sh

From 86c90027a3f42709941fbd389a58dc9478fa9adf Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 24 Sep 2025 09:41:42 +0100
Subject: [PATCH 08/30] chore: use run-on-host to build with docker

---
 .github/workflows/evaluation-multi-width-namespace.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index b21a2f51f5..225a50aa32 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -39,7 +39,7 @@ jobs:
           curl -LsSf https://astral.sh/uv/install.sh | sh
           # cd evaluation-multi-width-bv
           cp config.tiny.yaml config.yaml
-          ./run-on-container.sh
+          ./run-on-host.sh
 
       - name: Upload Warm Cache as Artifact
         uses: namespace-actions/upload-artifact@v1

From d8dc3a0060439c66ae89d40b1738e451c2b57250 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 24 Sep 2025 09:57:02 +0100
Subject: [PATCH 09/30] chore: ignore snakemake

---
 .github/workflows/evaluation-multi-width-namespace.yml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index 225a50aa32..573c8e915e 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -45,7 +45,10 @@ jobs:
         uses: namespace-actions/upload-artifact@v1
         with:
           name: evaluation-multi-width-bv-cache
-          path: .
+          path:
+            .
+            !./snakemake
+
           compression-level: 9
 
   run-full-eval:

From cd6b32100d765709217fb3e8d9b83652546302e2 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 24 Sep 2025 10:02:48 +0100
Subject: [PATCH 10/30] chore: fix paths

---
 .github/workflows/evaluation-multi-width-namespace.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index 573c8e915e..793b6c2f8a 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -45,7 +45,7 @@ jobs:
         uses: namespace-actions/upload-artifact@v1
         with:
           name: evaluation-multi-width-bv-cache
-          path:
+          path: |
             .
             !./snakemake
 

From ba8e196a1144345a6b9e284cee1f86c1090b494e Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 10:35:01 +0200
Subject: [PATCH 11/30] chore: update

---
 .../evaluation-multi-width-namespace.yml      | 148 +++++++++++++++---
 1 file changed, 128 insertions(+), 20 deletions(-)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index 793b6c2f8a..ea2cc32f01 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -10,8 +10,8 @@ permissions:
   id-token: write
 
 jobs:
-  warm-cache:
-    name: Warm Cache via MiniEval
+  run-batch:
+    name: Batch Run
     runs-on:
       - nscloud-ubuntu-24.04-amd64-16x32-with-cache
       - nscloud-cache-tag-my-custom-cache
@@ -32,28 +32,81 @@ jobs:
           ref: "master"
           token: ${{ secrets.NSCLOUD_GITHUB_TOKEN }}
 
-      - name: Run MiniEval
+      - name: Setup Ubuntu Dependencies
+        run: |
+          echo "set man-db/auto-update false" | sudo debconf-communicate && sudo dpkg-reconfigure man-db
+          sudo apt-get update
+          sudo apt-get install -y build-essential curl git python3 python3-pip unzip git gettext 
+
+      - name: Setup UV
+        run: |
+          # Install uv (assuming it's Python-based, via pip)
+          curl -LsSf https://astral.sh/uv/install.sh | sh
+
+          # Make uv available in all shells
+          echo "$HOME/.local/bin" >> $GITHUB_PATH
+
+      - name: Cache `.elan` folders
+        id: cache-lean
+        uses: actions/cache@v4
+        with:
+          path: |
+            ~/.elan
+          key: ${{ runner.os }}-elan-${{ hashFiles('leanharness/lean-toolchain') }}
+          restore-keys: |
+            ${{ runner.os }}-elan-${{ hashFiles('leanharness/lean-toolchain') }}
+
+      - name: Setup Elan
+        run: |
+          # Install elan (Lean version manager)
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+
+      - name: Make lake available
+        run: |
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Unzip goals
+        run: |
+          unzip -o goals.zip
+
+      - name: Run Minibatch
+        strategy:
+          matrix:
+            ibatch: [0, 1, 2]
+            nbatch: [3]
         run: |
           ls
+          pwd
           set -o pipefail
           curl -LsSf https://astral.sh/uv/install.sh | sh
-          # cd evaluation-multi-width-bv
           cp config.tiny.yaml config.yaml
-          ./run-on-host.sh
+          ./run-on-container.sh uv tool run snakemake run_minibatch --cores all --config nbatch=${{matrix.nbatch}} ibatch=${{matrix.ibatch}}
 
-      - name: Upload Warm Cache as Artifact
+      - name: Upload Data As Artifact
         uses: namespace-actions/upload-artifact@v1
         with:
-          name: evaluation-multi-width-bv-cache
+          name: ${{ github.run_id }}-ibatch-${{matrix.ibatch}}
+          retention-days: 1
           path: |
-            .
-            !./snakemake
-
+            autogenerated/*.jsonl
           compression-level: 9
 
-  run-full-eval:
-    needs: warm-cache
-    name: Run Full Evaluation
+      - name: Cache lake.
+        id: cache-lake
+        uses: actions/cache@v4
+        with:
+          path: |
+            leanharness/.lake
+          key: ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
+          restore-keys: |
+            ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
+
+
+  generate-plots:
+    needs: run-batch
+    name: Generate Reports
+    needs: run-batch
     runs-on:
       - nscloud-ubuntu-24.04-amd64-16x32-with-cache
       - nscloud-cache-tag-my-custom-cache
@@ -65,15 +118,70 @@ jobs:
       - name: Setup Ephemeral NS Cluster
         uses: namespacelabs/nscloud-setup@v0
 
-      - name: Download Warm Cache Artifact
-        uses: namespace-actions/download-artifact@v1
+      - name: Checkout Evaluation Repisitory via NS
+        uses: namespacelabs/nscloud-checkout-action@v7
+        with:
+          repository: "opencompl/evaluation-multi-width-bv"
+          ref: "master"
+          token: ${{ secrets.NSCLOUD_GITHUB_TOKEN }}
+
+      - name: Download data
+        uses: actions/download-artifact@v5
+        with:
+          path: autogenerated/
+          pattern: ${{ github.run_id }}-ibatch-*
+          merge-multiple: true
+
+      - name: Setup Ubuntu Dependencies
+        run: |
+          echo "set man-db/auto-update false" | sudo debconf-communicate && sudo dpkg-reconfigure man-db
+          sudo apt-get update
+          sudo apt-get install -y build-essential curl git python3 python3-pip unzip git gettext 
+
+      - name: Cache `.elan` folders
+        id: cache-lean
+        uses: actions/cache@v4
+        with:
+          path: |
+            ~/.elan
+          key: ${{ runner.os }}-elan-${{ hashFiles('leanharness/lean-toolchain') }}
+          restore-keys: |
+            ${{ runner.os }}-elan-${{ hashFiles('leanharness/lean-toolchain') }}
+
+      - name: Setup UV
+        run: |
+          # Install uv (assuming it's Python-based, via pip)
+          curl -LsSf https://astral.sh/uv/install.sh | sh
+
+          # Make uv available in all shells
+          echo "$HOME/.local/bin" >> $GITHUB_PATH
+
+      - name: Cache `.elan` folders
+        id: cache-lean
+        uses: actions/cache@v4
         with:
-          name: evaluation-multi-width-bv-cache
-          path: evaluation-multi-width-bv
+          path: |
+            ~/.elan
+          key: ${{ runner.os }}-elan-${{ hashFiles('leanharness/lean-toolchain') }}
+          restore-keys: |
+            ${{ runner.os }}-elan-${{ hashFiles('leanharness/lean-toolchain') }}
+
+      - name: Setup Elan
+        run: |
+          # Install elan (Lean version manager)
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+
+      - name: Make lake available
+        run: |
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      - name: Run Full Evaluateion
+      - name: Unzip goals
         run: |
-          cd evaluation-multi-width-bv
-          cp config.full.yaml config.yaml
+          unzip -o goals.zip
+
+      - name: Run Plotting Script
+        run: |
+          cp config.tiny.yaml config.yaml
           ./run-on-container.sh
 

From dec9368aa6f766697fe9457cb45786a7169cf846 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 10:40:05 +0200
Subject: [PATCH 12/30] chore: fix yaml

---
 .github/workflows/evaluation-multi-width-namespace.yml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index ea2cc32f01..be9485d814 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -1,4 +1,4 @@
-name: Evaluation Multi-Width (NS)
+name: +++ Evaluation Multi-Width (NS) +++
 on:
   push:
     branches:
@@ -106,7 +106,6 @@ jobs:
   generate-plots:
     needs: run-batch
     name: Generate Reports
-    needs: run-batch
     runs-on:
       - nscloud-ubuntu-24.04-amd64-16x32-with-cache
       - nscloud-cache-tag-my-custom-cache

From f931e693572fca463a1f6b5554439445ce254331 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 10:42:56 +0200
Subject: [PATCH 13/30] chore: fix yaml 2

---
 .github/workflows/evaluation-multi-width-namespace.yml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index be9485d814..8ff76887b4 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -20,6 +20,11 @@ jobs:
       - nscloud-container-image-cache
       - nscloud-runner-tool-cache-20gb
 
+    strategy:
+      matrix:
+        ibatch: [0, 1, 2]
+        nbatch: [3]
+
     steps:
       - name: Setup Ephemeral NS Cluster
         uses: namespacelabs/nscloud-setup@v0
@@ -71,10 +76,6 @@ jobs:
           unzip -o goals.zip
 
       - name: Run Minibatch
-        strategy:
-          matrix:
-            ibatch: [0, 1, 2]
-            nbatch: [3]
         run: |
           ls
           pwd

From d288737e2ac145869dd716b43a893e5af65c5d99 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 10:43:40 +0200
Subject: [PATCH 14/30] chore: fix yaml 3

---
 .github/workflows/evaluation-multi-width-namespace.yml | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/evaluation-multi-width-namespace.yml
index 8ff76887b4..cd6107418e 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/evaluation-multi-width-namespace.yml
@@ -138,16 +138,6 @@ jobs:
           sudo apt-get update
           sudo apt-get install -y build-essential curl git python3 python3-pip unzip git gettext 
 
-      - name: Cache `.elan` folders
-        id: cache-lean
-        uses: actions/cache@v4
-        with:
-          path: |
-            ~/.elan
-          key: ${{ runner.os }}-elan-${{ hashFiles('leanharness/lean-toolchain') }}
-          restore-keys: |
-            ${{ runner.os }}-elan-${{ hashFiles('leanharness/lean-toolchain') }}
-
       - name: Setup UV
         run: |
           # Install uv (assuming it's Python-based, via pip)

From b3055395a9569a239aa67afeb4e456f71170dd2f Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 10:47:07 +0200
Subject: [PATCH 15/30] chore: remove other GH action files so that this PR
 only spends time running the action I care about

---
 .github/workflows/automerge.yml              |  31 --
 .github/workflows/doc.yml                    |  43 --
 .github/workflows/docker.yml                 | 211 ---------
 .github/workflows/elan-gc.yml                |  10 -
 .github/workflows/evaluation-namespace.yml   | 347 ---------------
 .github/workflows/evaluation.yml             | 442 -------------------
 .github/workflows/update-mathlib-version.yml |  69 ---
 7 files changed, 1153 deletions(-)
 delete mode 100644 .github/workflows/automerge.yml
 delete mode 100644 .github/workflows/doc.yml
 delete mode 100644 .github/workflows/docker.yml
 delete mode 100644 .github/workflows/elan-gc.yml
 delete mode 100644 .github/workflows/evaluation-namespace.yml
 delete mode 100644 .github/workflows/evaluation.yml
 delete mode 100644 .github/workflows/update-mathlib-version.yml

diff --git a/.github/workflows/automerge.yml b/.github/workflows/automerge.yml
deleted file mode 100644
index c69cb3f7b0..0000000000
--- a/.github/workflows/automerge.yml
+++ /dev/null
@@ -1,31 +0,0 @@
-name: automerge
-on:
-  pull_request:
-    types:
-      - labeled
-      - unlabeled
-      - synchronize
-      - opened
-      - edited
-      - ready_for_review
-      - reopened
-      - unlocked
-  pull_request_review:
-    types:
-      - submitted
-  check_suite:
-    types:
-      - completed
-  status: {}
-jobs:
-  automerge:
-    runs-on: ubuntu-latest
-    permissions:
-      contents: write
-      pull-requests: write
-    steps:
-      - id: automerge
-        name: automerge
-        uses: "pascalgn/automerge-action@v0.16.4"
-        env:
-          GITHUB_TOKEN: "${{ secrets.GITHUB_TOKEN }}"
diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml
deleted file mode 100644
index 62d7b9efac..0000000000
--- a/.github/workflows/doc.yml
+++ /dev/null
@@ -1,43 +0,0 @@
-name: docs
-on:
-  push:
-    branches:
-      - "main-disabled"
-
-# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
-permissions:
-  contents: read
-  pages: write
-  id-token: write
-
-jobs:
-  build:
-    name: build and deploy documentation.
-    # Exclude expensive self-hosted runner. Reserved for performance benchmarking.
-    # https://docs.github.com/en/enterprise-cloud@latest/actions/writing-workflows/choosing-where-your-workflow-runs/choosing-the-runner-for-a-job#choosing-github-hosted-runners
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout 🛎️
-        uses: actions/checkout@v3
-
-      - name: Install elan 🕑
-        run: |
-          set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-          ~/.elan/bin/lean --version
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-  
-      - name: Generate docs 📜
-        run: |
-          ./docgen.sh
-
-# stolen from mathlib: https://github.com/leanprover-community/mathlib4_docs/blob/1f4ea7657bc377b4298fd400e567471d3a248b2d/.github/workflows/docs.yaml#L79-L86
-      - name: Upload artifact 📁
-        uses: actions/upload-pages-artifact@v1
-        with:
-          path: '.lake/build/doc'
-
-      - name: Deploy to GitHub Pages 🚀
-        id: deployment
-        uses: actions/deploy-pages@v1
-
diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
deleted file mode 100644
index 6879720c0b..0000000000
--- a/.github/workflows/docker.yml
+++ /dev/null
@@ -1,211 +0,0 @@
-name: Build & Evaluate (in Docker)
-on:
-  workflow_dispatch:
-  push:
-   branches:
-     - "main"
-  pull_request:
-  merge_group:
-
-# ^^ This workflow does not run automatically, to make sure we don't burn through too many
-# namespace.so credits. For now, it is only triggered manually if desired.
-
-permissions:
-  contents: write
-  packages: write
-
-jobs:
-  #
-  # Docker image builders
-  #
-  core-docker-img:
-    name: Build Docker image for core library
-    runs-on: namespace-profile-leanmlir-docker-cached
-    steps:
-      - name: Login to GitHub Container Registry
-        uses: docker/login-action@v3
-        with:
-          registry: ghcr.io
-          username: ${{ github.repository_owner }}
-          password: ${{ secrets.GITHUB_TOKEN }}
-
-      - name: Checkout 🛎️
-        uses: actions/checkout@v3
-
-      - name: Setup Docker metadata
-        id: meta
-        uses: docker/metadata-action@v5
-        with:
-          images: ghcr.io/opencompl/lean-mlir
-          tags: |
-            type=ref,event=branch
-            type=ref,event=pr
-            type=raw,value=${{ github.sha }}
-            type=raw,value=latest,enable={{is_default_branch}}
-
-      - name: Build and push
-        uses: docker/build-push-action@v6
-        with:
-          context: .
-          push: true
-          tags: ${{ steps.meta.outputs.tags }}
-          labels: ${{ steps.meta.outputs.labels }}
-
-#   instcombine-docker-img:
-#     name: Build Docker image for InstCombine Evaluation
-#     runs-on: ubuntu-latest # Run on GH-provided runner
-#     needs: core-docker-img
-#     steps:
-#       - name: Set up Docker Buildx
-#         uses: docker/setup-buildx-action@v3
-#
-#       - name: Login to GitHub Container Registry
-#         uses: docker/login-action@v3
-#         with:
-#           registry: ghcr.io
-#           username: ${{ github.repository_owner }}
-#           password: ${{ secrets.GITHUB_TOKEN }}
-#
-#       - name: Checkout 🛎️
-#         uses: actions/checkout@v3
-#
-#       - name: Setup Docker metadata
-#         id: meta
-#         uses: docker/metadata-action@v5
-#         with:
-#           images: ghcr.io/opencompl/lean-mlir-instcombine
-#           tags: |
-#             type=ref,event=branch
-#             type=ref,event=pr
-#             type=raw,value=${{ github.sha }}
-#             type=raw,value=latest,enable={{is_default_branch}}
-#
-#       - name: Build and push Docker image
-#         uses: docker/build-push-action@v6
-#         with:
-#           context: "./bv-evaluation"
-#           build-args: |
-#             LEANMLIR_TAG=${{ github.sha }}
-#           push: true
-#           tags: ${{ steps.meta.outputs.tags }}
-#           labels: ${{ steps.meta.outputs.labels }}
-#           cache-from: type=gha
-#           cache-to: type=gha,mode=max
-
-  #
-  # Evaluation & test jobs
-  #
-  build-tools:
-    name: use docker (runs on namespace)
-    runs-on: namespace-profile-leanmlir-docker-cached
-    needs: core-docker-img
-    container: "ghcr.io/opencompl/lean-mlir:${{ github.sha }}"
-    defaults:
-      run:
-        working-directory: /code/lean-mlir
-    steps:
-      - name: Symlink .elan (to correct for GHA changing $HOME)
-        run: '[ -e ~/.elan ] || ln -s /root/.elan ~/.elan'
-      - name: Run lake build
-        run: |
-          lake -R build
-
-  build-tools-github:
-    name: use docker (runs on GitHub)
-    runs-on: ubuntu-latest # Run on GH-provided runner
-    needs: core-docker-img
-    container: "ghcr.io/opencompl/lean-mlir:${{ github.sha }}"
-    defaults:
-      run:
-        working-directory: /code/lean-mlir
-    steps:
-      - name: Symlink .elan (to correct for GHA changing $HOME)
-        run: '[ -e ~/.elan ] || ln -s /root/.elan ~/.elan'
-      - name: Run lake build
-        run: |
-          lake -R build
-
-#   alive-check-changes:
-#     name: Check for changes in AliveStatements
-#     runs-on: ubuntu-latest # Run on GH-provided runner
-#     needs: instcombine-docker-img
-#     container: "ghcr.io/opencompl/lean-mlir-instcombine:${{ github.sha }}"
-#     defaults:
-#       run:
-#         working-directory: /code/lean-mlir
-#     steps:
-#       - name: Symlink .elan (to correct for GHA changing $HOME)
-#         run: '[ -e ~/.elan ] || ln -s /root/.elan ~/.elan'
-#
-#       - run: |
-#           lake build AliveExamples
-#           (cd SSA/Projects/InstCombine/; uv run ./update_alive_statements.py)
-#           # /--------------------------- ^^^^^^
-#           # | TODO: this could be removed if we add a uv shebang to the python file
-#           bash -c '! git diff -- SSA/Projects/InstCombine | grep .'  # iff git diff is empty, 'grep .' fails, '!' inverts the failure, and in the forced bash
-#
-#   evaluation-LLVM:
-#     name: Evaluate LLVM
-#     runs-on: ubuntu-latest # Run on GH-provided runner
-#     needs: instcombine-docker-img
-#     container: "ghcr.io/opencompl/lean-mlir-instcombine:${{ github.sha }}"
-#     defaults:
-#       run:
-#         working-directory: /code/lean-mlir/bv-evaluation
-#     permissions:
-#       pull-requests: write
-#     steps:
-#       - name: Symlink .elan (to correct for GHA changing $HOME)
-#         run: '[ -e ~/.elan ] || ln -s /root/.elan ~/.elan'
-#
-#       - name: Run LLVM
-#         continue-on-error: true
-#         run: |
-#           uv run ./compare.py instcombine -j48 \
-#             || (echo "LEANMLIR_STATUS=fail" >> $GITHUB_ENV; exit 1)
-#
-#       - name: Collect data LLVM
-#         continue-on-error: true
-#         run: |
-#           (uv run ./collect.py instcombine | tee llvm-stats) \
-#             || (echo "LEANMLIR_STATUS=fail" >> $GITHUB_ENV; exit 1)
-#
-#       - uses: actions/github-script@v6
-#         if: env.LEANMLIR_STATUS != 'fail' && github.event_name == 'pull_request'
-#         with:
-#           script: |
-#             const fs = require('fs')
-#             github.rest.issues.createComment({
-#               issue_number: context.issue.number,
-#               owner: context.repo.owner,
-#               repo: context.repo.repo,
-#               body: fs.readFileSync('/code/lean-mlir/bv-evaluation/llvm-stats', 'utf8')
-#             })
-#
-#       - name: Upload LLVM artifact
-#         uses: actions/upload-artifact@v4
-#         with:
-#           name: LLVM evaluation
-#           path: results
-#
-#   extract-goals:
-#     name: Extract goals
-#     runs-on: ubuntu-latest # Run on GH-provided runner
-#     needs: instcombine-docker-img
-#     container: "ghcr.io/opencompl/lean-mlir-instcombine:${{ github.sha }}"
-#     defaults:
-#       run:
-#         working-directory: /code/lean-mlir
-#     strategy:
-#       matrix:
-#         extract_offset: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
-#         extract_stride: [10]
-#     steps:
-#       - name: Symlink .elan (to correct for GHA changing $HOME)
-#         run: '[ -e ~/.elan ] || ln -s /root/.elan ~/.elan'
-#
-#       - name: Ensure InstCombine goals are up-to-date
-#         env:
-#           GIT_DIR: ${{ github.workspace }}/.git
-#         run: |
-#           bash SSA/Projects/InstCombine/scripts/test-extract-goals.sh --nfiles 9000 -j7  --stride ${{matrix.extract_stride}} --offset ${{matrix.extract_offset}}
diff --git a/.github/workflows/elan-gc.yml b/.github/workflows/elan-gc.yml
deleted file mode 100644
index 4672b1aa7d..0000000000
--- a/.github/workflows/elan-gc.yml
+++ /dev/null
@@ -1,10 +0,0 @@
-name: Garbage collect elan toolchains
-on:
-  schedule:
-    - cron: '0 9 * * 1' # Run weekly, at 09:00 on Monday
-
-jobs:
-  elan-gc:
-    runs-on: self-hosted
-    steps:
-      - run: elan toolchain gc --delete
diff --git a/.github/workflows/evaluation-namespace.yml b/.github/workflows/evaluation-namespace.yml
deleted file mode 100644
index 9ce3322ebb..0000000000
--- a/.github/workflows/evaluation-namespace.yml
+++ /dev/null
@@ -1,347 +0,0 @@
-name: Evaluation (Namespace) - Experimental
-on:
-  push:
-    branches:
-      - "main"
-  pull_request:
-
-permissions:
-  contents: write
-
-jobs:
-  build:
-    name: Build Lean-MLIR on NS
-    runs-on:
-      - nscloud-ubuntu-24.04-amd64-16x32-with-cache
-      - nscloud-cache-tag-my-custom-cache
-      - nscloud-cache-size-100gb
-      - nscloud-git-mirror-5gb
-      - nscloud-container-image-cache
-      - nscloud-runner-tool-cache-20gb
-
-    steps:
-      - name: Checkout code (use nscloud)
-        uses: namespacelabs/nscloud-checkout-action@v7
-
-      - name: Cache Elan && Lake Folders
-        uses: namespacelabs/nscloud-cache-action@v1
-        with:
-          path: |
-            ~/.elan
-            .lake
-            Blase/.lake
-            TacBench/.lake
-
-      - name: Install Elan & Lean
-        run: |
-          set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-          ~/.elan/bin/lean --version
-
-      - name: Make lake available
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Build Lean-MLIR & Mathlib
-        # We build Mathlib from scratch as this reduces the build artifacts that are stored in the cache. Previous experiments
-        # led to savings from avoiding a full Mathlib cache in the order of a couple hundred MBs.
-        run: |
-          lake -R build
-
-  test-blase:
-    name: Test Blase
-    runs-on:
-      - nscloud-ubuntu-24.04-amd64-16x32-with-cache
-      - nscloud-cache-tag-my-custom-cache
-      - nscloud-cache-size-100gb
-      - nscloud-git-mirror-5gb
-      - nscloud-container-image-cache
-      - nscloud-runner-tool-cache-20gb
-      - nscloud-cache-exp-do-not-commit
-
-    needs: build
-    permissions:
-      pull-requests: write
-    steps:
-      - name: Checkout code (use nscloud)
-        uses: namespacelabs/nscloud-checkout-action@v7
-
-      - name: Cache Elan && Lake Folders
-        uses: namespacelabs/nscloud-cache-action@v1
-        with:
-          path: |
-            ~/.elan
-            .lake
-            Blase/.lake
-            TacBench/.lake
-
-      - name: Install Elan & Lean
-        run: |
-          set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-          ~/.elan/bin/lean --version
-
-      - name: Add Lean to PATH
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Build Lean-MLIR (should be all in cache)
-        run: |
-          lake -R build
-
-      - name: Run Blase Test Suite
-        run: |
-          lake build BlaseTest
-
-  build-github-action-cache:
-    name: Build Lean-MLIR on NS (GitHub Action Cache)
-    runs-on:
-      - nscloud-ubuntu-24.04-amd64-16x32-with-cache
-      - nscloud-cache-tag-my-custom-cache-2
-      - nscloud-cache-size-100gb
-      - nscloud-git-mirror-5gb
-      - nscloud-container-image-cache
-      - nscloud-runner-tool-cache-20gb
-
-    steps:
-      - name: Checkout code (use nscloud)
-        uses: namespacelabs/nscloud-checkout-action@v7
-
-      - name: Cache Elan && Lake Folders
-        uses: namespacelabs/nscloud-cache-action@v1
-        with:
-          path: |
-            ~/.elan
-            .lake
-            Blase/.lake
-            TacBench/.lake
-
-      - name: Install Elan & Lean
-        run: |
-          set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-          ~/.elan/bin/lean --version
-
-      - name: Make lake available
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Build Lean-MLIR & Mathlib
-        # We build Mathlib from scratch as this reduces the build artifacts that are stored in the cache. Previous experiments
-        # led to savings from avoiding a full Mathlib cache in the order of a couple hundred MBs.
-        run: |
-          lake -R build
-
-      - name: Cache `.lake` folders
-        id: cache-lake
-        uses: actions/cache/save@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-            */.lake
-          key: nstest-gac-${{ runner.os }}-lake-packages-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-
-      - name: Cache `.elan` folders
-        id: cache-lean-restore
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            ~/.elan
-          key: nstest-gac-${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-          lookup-only: true
-
-      - name: Cache `.elan` folders
-        id: cache-lean
-        if: steps.cache-lean-restore.outputs.cache-hit != 'true'
-        uses: actions/cache/save@v4
-        with:
-          path: |
-            ~/.elan
-          key: nstest-gac-${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-
-
-  test-blase-github-action-cache:
-    name: Test Blase (GitHub Action Cache)
-    runs-on:
-      - nscloud-ubuntu-24.04-amd64-16x32-with-cache
-      - nscloud-cache-tag-my-custom-cache-2
-      - nscloud-cache-size-100gb
-      - nscloud-git-mirror-5gb
-      - nscloud-container-image-cache
-      - nscloud-runner-tool-cache-20gb
-      - nscloud-cache-exp-do-not-commit
-
-    needs: build-github-action-cache
-    permissions:
-      pull-requests: write
-    steps:
-      - name: Checkout code (use nscloud)
-        uses: namespacelabs/nscloud-checkout-action@v7
-
-      - name: Load Lean from Cache
-        id: cache-lean
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            ~/.elan
-          key: nstest-gac-${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-
-      - name: Load Lean-MLIR from Cache
-        id: cache-lake
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-            */.lake
-          key: nstest-gac-${{ runner.os }}-lake-packages-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-
-      - name: Install Elan & Lean
-        run: |
-          set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-          ~/.elan/bin/lean --version
-
-      - name: Add Lean to PATH
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Build Lean-MLIR (should be all in cache)
-        run: |
-          lake -R build
-
-      - name: Run Blase Test Suite
-        run: |
-          lake build BlaseTest
-
-
-  build-ns-artifact:
-    name: Build Lean-MLIR on NS (Namespace Artifact)
-    runs-on:
-      - nscloud-ubuntu-24.04-amd64-16x32-with-cache
-      - nscloud-cache-tag-my-custom-cache-3
-      - nscloud-cache-size-100gb
-      - nscloud-git-mirror-5gb
-      - nscloud-container-image-cache
-      - nscloud-runner-tool-cache-20gb
-
-    steps:
-      - name: Checkout code (use nscloud)
-        uses: namespacelabs/nscloud-checkout-action@v7
-
-      - name: Cache Elan && Lake Folders
-        uses: namespacelabs/nscloud-cache-action@v1
-        with:
-          path: |
-            ~/.elan
-            .lake
-            Blase/.lake
-            TacBench/.lake
-
-      - name: Install Elan & Lean
-        run: |
-          set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-          ~/.elan/bin/lean --version
-
-      - name: Make lake available
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Build Lean-MLIR & Mathlib
-        # We build Mathlib from scratch as this reduces the build artifacts that are stored in the cache. Previous experiments
-        # led to savings from avoiding a full Mathlib cache in the order of a couple hundred MBs.
-        run: |
-          lake -R build
-
-      - name: Cache `.lake` folders
-        id: cache-lake
-        uses: actions/cache/save@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-            */.lake
-          key: nstest-gac-${{ runner.os }}-lake-packages-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-
-      - name: Upload Archive
-        uses: namespace-actions/upload-artifact@v1
-        with:
-          name: lake-folder
-          path: |
-            .lake/packages
-            .lake/build
-            */.lake
-
-      - name: Cache `.elan` folders
-        id: cache-lean-restore
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            ~/.elan
-          key: nstest-gac-${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-          lookup-only: true
-
-      - name: Cache `.elan` folders
-        id: cache-lean
-        if: steps.cache-lean-restore.outputs.cache-hit != 'true'
-        uses: actions/cache/save@v4
-        with:
-          path: |
-            ~/.elan
-          key: nstest-gac-${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-
-
-  test-blase-ns-artifact:
-    name: Test Blase (Namespace Aritfact)
-    runs-on:
-      - nscloud-ubuntu-24.04-amd64-16x32-with-cache
-      - nscloud-cache-tag-my-custom-cache-3
-      - nscloud-cache-size-100gb
-      - nscloud-git-mirror-5gb
-      - nscloud-container-image-cache
-      - nscloud-runner-tool-cache-20gb
-      - nscloud-cache-exp-do-not-commit
-
-    needs: build-ns-artifact
-    permissions:
-      pull-requests: write
-    steps:
-      - name: Checkout code (use nscloud)
-        uses: namespacelabs/nscloud-checkout-action@v7
-
-      - name: Load Lean from Cache
-        id: cache-lean
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            ~/.elan
-          key: nstest-gac-${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-
-      - name: Download Archive
-        uses: namespace-actions/download-artifact@v1
-        with:
-          name: lake-folder
-          path: |
-            .lake/packages
-            .lake/build
-            */.lake
-
-      - name: Install Elan & Lean
-        run: |
-          set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-          ~/.elan/bin/lean --version
-
-      - name: Add Lean to PATH
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Build Lean-MLIR (should be all in cache)
-        run: |
-          lake -R build
-
-      - name: Run Blase Test Suite
-        run: |
-          lake build BlaseTest
diff --git a/.github/workflows/evaluation.yml b/.github/workflows/evaluation.yml
deleted file mode 100644
index 11e819287a..0000000000
--- a/.github/workflows/evaluation.yml
+++ /dev/null
@@ -1,442 +0,0 @@
-name: Evaluation
-on:
-  push:
-    branches:
-      - "main"
-  pull_request:
-
-permissions:
-  contents: write
-
-jobs:
-  eval-build:
-    name: Build Lean-MLIR
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout 🛎️
-        uses: actions/checkout@v3
-
-      - name: Cache `.elan` folders
-        id: cache-lean
-        uses: actions/cache@v4
-        with:
-          path: |
-            ~/.elan
-          key: ${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-          restore-keys: |
-            ${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-
-      - name: Install Elan & Lean
-        if: steps.cache-lean.outputs.cache-hit != 'true'
-        run: |
-          set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-          ~/.elan/bin/lean --version
-
-      - name: Make lake available
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Cache `.lake` folders
-        id: cache-lake
-        uses: actions/cache@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-            */.lake
-          key: ${{ runner.os }}-lake-packages-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-          restore-keys: |
-            ${{ runner.os }}-lake-packages-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-            ${{ runner.os }}-lake-packages-${{ hashFiles('lake-manifest.json') }}
-
-      - name: Build Lean-MLIR & Mathlib
-        # We build Mathlib from scratch as this reduces the build artifacts that are stored in the cache. Previous experiments
-        # led to savings from avoiding a full Mathlib cache in the order of a couple hundred MBs.
-        run: |
-          lake -R build
-
-  extract-goals:
-    name: Extract goals
-    runs-on: ubuntu-latest
-    needs: eval-build
-    strategy:
-      matrix:
-        extract_offset: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
-        extract_stride: [10]
-    permissions:
-      pull-requests: write
-    steps:
-      - name: Checkout 🛎️
-        uses: actions/checkout@v3
-
-      - name: Load Lean from Cache
-        id: cache-lean
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            ~/.elan
-          key: ${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-
-      - name: Load Lean-MLIR from Cache
-        id: cache-lake
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-            */.lake
-          key: ${{ runner.os }}-lake-packages-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-
-      - name: Add Lean to PATH
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Build Lean-MLIR (should be all in cache)
-        run: |
-          lake -R build
-
-      - name: Ensure InstCombine goals are up-to-date
-        run: |
-          bash SSA/Projects/InstCombine/scripts/test-extract-goals.sh --nfiles 9000 -j7  --stride ${{matrix.extract_stride}} --offset ${{matrix.extract_offset}}
-
-  test-blase:
-    name: Test Blase
-    runs-on: ubuntu-latest
-    needs: eval-build
-    permissions:
-      pull-requests: write
-    steps:
-      - name: Checkout 🛎️
-        uses: actions/checkout@v3
-
-      - name: Load Lean from Cache
-        id: cache-lean
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            ~/.elan
-          key: ${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-
-      - name: Load Lean-MLIR from Cache
-        id: cache-lake
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-            */.lake
-          key: ${{ runner.os }}-lake-packages-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-
-      - name: Add Lean to PATH
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Build Lean-MLIR (should be all in cache)
-        run: |
-          lake -R build
-
-      - name: Run Blase Test Suite
-        run: |
-          lake build BlaseTest
-
-  evaluation-LLVM:
-    name: Evaluate LLVM
-    runs-on: ubuntu-latest
-    needs: eval-build
-    permissions:
-      pull-requests: write
-    steps:
-      - name: Checkout 🛎️
-        uses: actions/checkout@v3
-
-      - name: Load Lean from Cache
-        id: cache-lean
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            ~/.elan
-          key: ${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-
-      - name: Load Lean-MLIR from Cache
-        id: cache-lake
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-            */.lake
-          key: ${{ runner.os }}-lake-packages-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-
-      - name: Add Lean to PATH
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Build Lean-MLIR (should be all in cache)
-        run: |
-          lake -R build
-
-      - name: Install Python Modules
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y python3-matplotlib python3-pandas python3-num2words python3-psutil ripgrep
-
-      - name: Run LLVM
-        continue-on-error: true
-        run: |
-          cd bv-evaluation
-          python3 ./compare.py instcombine -j48 \
-            || (echo "LEANMLIR_STATUS=fail" >> $GITHUB_ENV; exit 1)
-
-      - name: Collect data LLVM
-        continue-on-error: true
-        run: |
-          cd bv-evaluation
-          (python3 ./collect.py instcombine | tee llvm-stats) \
-            || (echo "LEANMLIR_STATUS=fail" >> $GITHUB_ENV; exit 1)
-
-      - uses: actions/github-script@v6
-        if: env.LEANMLIR_STATUS != 'fail' && github.event_name == 'pull_request'
-        with:
-          script: |
-            const fs = require('fs')
-            github.rest.issues.createComment({
-              issue_number: context.issue.number,
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              body: fs.readFileSync('bv-evaluation/llvm-stats', 'utf8')
-            })
-
-      - name: Upload LLVM artifact
-        uses: actions/upload-artifact@v4
-        with:
-          name: LLVM evaluation
-          path: bv-evaluation/results
-
-  test-tools-scaling-auto-generated-stmts:
-    name: Test tools, scaling, and auto-generated statements
-    runs-on: ubuntu-latest
-    needs: eval-build
-    permissions:
-      pull-requests: write
-    steps:
-      - name: Checkout 🛎️
-        uses: actions/checkout@v3
-
-      - name: Load Lean from Cache
-        id: cache-lean
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            ~/.elan
-          key: ${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-
-      - name: Load Lean-MLIR from Cache
-        id: cache-lake
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-            */.lake
-          key: ${{ runner.os }}-lake-packages-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-
-      - name: Add Lean to PATH
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Build Lean-MLIR (should be all in cache)
-        run: |
-          lake -R build
-          
-      - name: Compile `mlirnatural` Executable 🧐
-        run: |
-          lake -R build mlirnatural
-
-      - name: Compile `opt` Executable 🧐
-        run: |
-          lake -R build opt
-
-      - name: Compile `LLVMRiscV` Tests 
-        run: |
-          lake -R build SSA.Projects.LLVMRiscV.Tests.Tests
-
-#      This broke the build during a recent update
-#      - name: LLVM opt round trip test
-#        run: |
-#          lake exec opt test/LLVMDialect/InstCombine/bb0.mlir
-      
-      - name: Compile ISL
-        run: |
-          lake -R build ISL
-
-      - name: Compile Alive Scaling
-        run: |
-          lake -R build SSA.Projects.InstCombine.ScalingTest
-
-      - name: Check for changes in AliveStatements
-        run: |
-          lake build AliveExamples
-          (cd SSA/Projects/InstCombine/; ./update_alive_statements.py)
-          bash -c '! git diff | grep .'  # iff git diff is empty, 'grep .' fails, '!' inverts the failure, and in the forced bash
-          
-  test-core-library:
-    name: Test Core Library
-    runs-on: ubuntu-latest
-    needs: eval-build
-    permissions:
-      pull-requests: write
-    steps:
-      - name: Checkout 🛎️
-        uses: actions/checkout@v3
-
-      - name: Load Lean from Cache
-        id: cache-lean
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            ~/.elan
-          key: ${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-
-      - name: Load Lean-MLIR from Cache
-        id: cache-lake
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-            */.lake
-          key: ${{ runner.os }}-lake-packages-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-
-      - name: Add Lean to PATH
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Build Lean-MLIR (should be all in cache)
-        run: |
-          lake -R build
-
-      - name: Test Core Library
-        run: |
-          lake -R build SSA.Tests.Tests
-
-      - name: Test InstCombine (unit-tests)
-        run: |
-          lake -R build SSA.Projects.InstCombine.Tests.Tests
-
-      - name: Compile Decide Experiment 🧐
-        run: |
-          lake -R build Blase.Fast.Decide
-
-      - name: Compile Hacker's Delight Theorems 🧮
-        run: |
-          sed -i -E 's/WIDTH/16/' SSA/Projects/InstCombine/HackersDelight/ch2_1DeMorgan.lean
-          sed -i -E 's/WIDTH/16/' SSA/Projects/InstCombine/HackersDelight/ch2_2AdditionAndLogicalOps.lean
-          lake -R build SSA.Projects.InstCombine.HackersDelight.ch2_1DeMorgan # compile and check the Hacker's Delight theorems chapter 2-1
-          lake -R build SSA.Projects.InstCombine.HackersDelight.ch2_2AdditionAndLogicalOps # compile and check the Hacker's Delight theorems chapter 2-2
-          sed -i -E 's/16/WIDTH/' SSA/Projects/InstCombine/HackersDelight/ch2_1DeMorgan.lean
-          sed -i -E 's/16/WIDTH/' SSA/Projects/InstCombine/HackersDelight/ch2_2AdditionAndLogicalOps.lean
-
-      - name: Compile Alive Examples
-        run: |
-          lake -R build SSA.Projects.InstCombine.AliveAutoGenerated
-          sed -i 's/set_option warn.sorry false/set_option warn.sorry true/' SSA/Projects/InstCombine/AliveStatements.lean
-          lake -R build SSA.Projects.InstCombine.AliveStatements 2>&1 | tee out
-          git checkout SSA/Projects/InstCombine/AliveStatements.lean
-          echo `grep theorem SSA/Projects/InstCombine/AliveStatements.lean | wc -l` > all
-          grep 'Alive.*sorry' out | wc -l > failed
-          x=$((`cat all`  -  `cat failed`)); echo $x > diff
-          echo "ALIVE_SUCCESS=$(cat diff)" >> $GITHUB_ENV
-          echo "ALIVE_ALL=$(cat all)" >> $GITHUB_ENV
-          echo "ALIVE_FAILED=$(cat failed)" >> $GITHUB_ENV
-
-      - name: Compile Alive Examples (With UB)
-        run: |
-          lake -R build SSA.Projects.SLLVM.Evaluation.AliveAutoGeneratedCopy
-
-      - name: Compile CIRCT Dialects (DC/Handshake)
-        run: |
-          lake -R build CIRCT
-
-      - if: github.event_name == 'pull_request'
-        run: |
-          echo "Alive Statistics: ${{env.ALIVE_SUCCESS}} / ${{env.ALIVE_ALL}} (${{env.ALIVE_FAILED}} failed)"
-          if  [ "${{env.ALIVE_SUCCESS}}" -ne "90" ] ||
-              [ "${{env.ALIVE_ALL}}" -ne "93" ] ||
-              [ "${{env.ALIVE_FAILED}}" -ne "3" ]; then
-            echo "ERROR: Alive statistics do not match the expected values!"
-            exit 1
-          fi
-
-  evaluation-alive-hdel:
-    name: Evaluation Alive and Hacker's Delight
-    runs-on: ubuntu-latest
-    needs: eval-build
-    permissions:
-      pull-requests: write
-    steps:
-      - name: Checkout 🛎️
-        uses: actions/checkout@v3
-
-      - name: Load Lean from Cache
-        id: cache-lean
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            ~/.elan
-          key: ${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
-
-      - name: Load Lean-MLIR from Cache
-        id: cache-lake
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-            */.lake
-          key: ${{ runner.os }}-lake-packages-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-
-      - name: Add Lean to PATH
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Build Lean-MLIR (should be all in cache)
-        run: |
-          lake -R build
-
-      - name: Install Python Modules
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y python3-matplotlib python3-pandas python3-num2words python3-psutil ripgrep
-
-      - name: Run Alive Symbolic
-        run: |
-          (cd bv-evaluation; python3 ./compare-leansat-vs-bitwuzla-alive-sym.py -j48)
-
-      - name: Compare Alive All
-        continue-on-error: true
-        run: |
-          (cd bv-evaluation; python3 ./collect-data-alive.py > /dev/null)
-
-      - name: Run HDel Symbolic
-        run: |
-          (cd bv-evaluation; python3 ./compare-leansat-vs-bitwuzla-hdel-sym.py -j48)
-
-      - name: Compare HDEl Symbolic
-        continue-on-error: true
-        run: |
-          (cd bv-evaluation; python3 ./collect-data-hdel-symbolic.py > /dev/null)
-
-      - name: Run HDel
-        run: |
-          (cd bv-evaluation; python3 ./compare.py hackersdelight -j48)
-
-      - name: Collect data HDEl
-        continue-on-error: true
-        run: |
-          (cd bv-evaluation; python3 ./collect.py hackersdelight > /dev/null)
-
-      - name: Collect Stats
-        continue-on-error: true
-        run: |
-          (cd bv-evaluation/tools; python3 ./collect-stats-bv-decide.py)
diff --git a/.github/workflows/update-mathlib-version.yml b/.github/workflows/update-mathlib-version.yml
deleted file mode 100644
index 1b746c8e2e..0000000000
--- a/.github/workflows/update-mathlib-version.yml
+++ /dev/null
@@ -1,69 +0,0 @@
-name: Update mathlib version
-on:
-  schedule:
-    - cron: '44 * * * *'
-  workflow_dispatch:
-
-permissions: write-all
-
-jobs:
-  mathlibtoday:
-    name: Update Mathlib & Lean
-    strategy:
-      fail-fast: false
-      matrix:
-        daysbefore: [0, 1, 2, 3, 4, 5, 6, 7, 8]
-    permissions: write-all
-    # Exclude expensive self-hosted runner. Reserved for performance benchmarking.
-    # https://docs.github.com/en/enterprise-cloud@latest/actions/writing-workflows/choosing-where-your-workflow-runs/choosing-the-runner-for-a-job#choosing-github-hosted-runners
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout 🛎️
-        uses: actions/checkout@v4
-        with:
-          token: ${{secrets.PAT}}
-
-      - name: Install elan 🕑
-        run: |
-          set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-          ~/.elan/bin/lean --version
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Get Mathlib Date
-        id: mldate
-        run: |
-           echo "date=`date -d '-${{matrix.daysbefore}} day' +20%y-%m-%d`"
-           echo "date=`date -d '-${{matrix.daysbefore}} day' +20%y-%m-%d`" >> $GITHUB_OUTPUT
-
-      - name: install zsh
-        run: |
-          sudo apt-get update; sudo apt-get install zsh
-
-      - name: Check if lean toolchain is already newer or equally old
-        shell: zsh {0}
-        run: |
-           if [[ `cat lean-toolchain | sed -e 's/leanprover\/lean4:nightly-//' | sed -e '/$^/d' | sed -e 's/-//g' ` -ge `echo ${{steps.mldate.outputs.date}} | sed -e 's/-//g'` ]]; then echo "abort: lean-toolchain is newer than proposed date"; false ; fi
-
-      - name: Set Mathlib Date
-        run: |
-           sed -e "s/\"nightly-testing.*\"/\"nightly-testing-${{steps.mldate.outputs.date}}\"/" -i lakefile.toml
-           sed -e "s/nightly.*/nightly-${{steps.mldate.outputs.date}}/" -i lean-toolchain
-           echo "## lakefile.toml"
-           cat lakefile.toml
-           echo "## lean-toolchain"
-           cat lean-toolchain
-           lake update mathlib
-
-      - name: Merge pre-existing pull request
-        continue-on-error: true
-        run: |
-           git merge origin/auto-mathlib-update-${{steps.mldate.outputs.date}}
-
-      - name: Create Pull Request
-        uses: peter-evans/create-pull-request@v7
-        with:
-          title: "${{steps.mldate.outputs.date}} lean nightly update"
-          branch: "auto-mathlib-update-${{steps.mldate.outputs.date}}"
-          body: "automatic update of mathlib + lean via GitHub action."
-          token: ${{secrets.PAT}}

From b1eae4f9f78c48da1ba0c797f2bb469c57958cf8 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 10:47:17 +0200
Subject: [PATCH 16/30] chore: remove other GH action files so that this PR
 only spends time running the action I care about

---
 .github/workflows/medusa.yml | 56 ------------------------------------
 1 file changed, 56 deletions(-)
 delete mode 100644 .github/workflows/medusa.yml

diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml
deleted file mode 100644
index e581b66aeb..0000000000
--- a/.github/workflows/medusa.yml
+++ /dev/null
@@ -1,56 +0,0 @@
-name: Medusa Build & Test
-on:
-  push:
-    branches:
-      - "main"
-    paths:
-      - 'Medusa/**'
-  pull_request:
-    paths:
-      - 'Medusa/**'
-
-  merge_group:
-
-permissions:
-  contents: write
-  packages: write
-
-jobs:
-  build:
-    name: medusa
-    permissions:
-      pull-requests: write
-    # Exclude expensive self-hosted runner. Reserved for performance benchmarking.
-    # https://docs.github.com/en/enterprise-cloud@latest/actions/writing-workflows/choosing-where-your-workflow-runs/choosing-the-runner-for-a-job#choosing-github-hosted-runners
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout 🛎️
-        uses: actions/checkout@v3
-
-      - name: Install elan 🕑
-        run: |
-          set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-          ~/.elan/bin/lean --version
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Cache `.lake` folder
-        id: cache-lake
-        uses: actions/cache@v4
-        with:
-          path: Medusa/.lake
-          key: ${{ runner.os }}-lake-${{ hashFiles('Medusa/lake-manifest.json') }}-4
-
-      - name: Get mathlib cache (only if no cache available)
-        if: steps.cache-lake.outputs.cache-hit != 'true'
-        continue-on-error: true
-        run: |
-          (pushd Medusa; lake -R exe cache get; true; popd) # download cache of mathlib docs.
-
-      - name: Compile Medusa
-        run: |
-          pushd Medusa; lake -R build Medusa --iofail
-
-      - name: Test Medusa
-        run: |
-          pushd Medusa; lake test; popd

From 374c42ce92a16d2e1a063c20fb67dcbc3790809a Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 10:50:43 +0200
Subject: [PATCH 17/30] chore: rename to cluster-scale eval to be clear

chore: move lake cache to before
---
 ...e.yml => cluster-scale-multi-width-ns.yml} | 38 +++++++++++++------
 1 file changed, 26 insertions(+), 12 deletions(-)
 rename .github/workflows/{evaluation-multi-width-namespace.yml => cluster-scale-multi-width-ns.yml} (87%)

diff --git a/.github/workflows/evaluation-multi-width-namespace.yml b/.github/workflows/cluster-scale-multi-width-ns.yml
similarity index 87%
rename from .github/workflows/evaluation-multi-width-namespace.yml
rename to .github/workflows/cluster-scale-multi-width-ns.yml
index cd6107418e..2387995a8b 100644
--- a/.github/workflows/evaluation-multi-width-namespace.yml
+++ b/.github/workflows/cluster-scale-multi-width-ns.yml
@@ -1,4 +1,4 @@
-name: +++ Evaluation Multi-Width (NS) +++
+name: +++ Cluster-Scale Multi-Width (NS) +++
 on:
   push:
     branches:
@@ -70,6 +70,17 @@ jobs:
       - name: Make lake available
         run: |
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
+          pushd leanharness; lake build; popd
+
+      - name: Cache lake.
+        id: cache-lake
+        uses: actions/cache@v4
+        with:
+          path: |
+            leanharness/.lake
+          key: ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
+          restore-keys: |
+            ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
 
       - name: Unzip goals
         run: |
@@ -82,7 +93,7 @@ jobs:
           set -o pipefail
           curl -LsSf https://astral.sh/uv/install.sh | sh
           cp config.tiny.yaml config.yaml
-          ./run-on-container.sh uv tool run snakemake run_minibatch --cores all --config nbatch=${{matrix.nbatch}} ibatch=${{matrix.ibatch}}
+          uv tool run snakemake run_minibatch --cores all --config nbatch=${{matrix.nbatch}} ibatch=${{matrix.ibatch}}
 
       - name: Upload Data As Artifact
         uses: namespace-actions/upload-artifact@v1
@@ -93,15 +104,6 @@ jobs:
             autogenerated/*.jsonl
           compression-level: 9
 
-      - name: Cache lake.
-        id: cache-lake
-        uses: actions/cache@v4
-        with:
-          path: |
-            leanharness/.lake
-          key: ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
-          restore-keys: |
-            ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
 
 
   generate-plots:
@@ -165,6 +167,17 @@ jobs:
       - name: Make lake available
         run: |
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
+          pushd leanharness; lake build; popd
+
+      - name: Cache lake.
+        id: cache-lake
+        uses: actions/cache@v4
+        with:
+          path: |
+            leanharness/.lake
+          key: ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
+          restore-keys: |
+            ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
 
       - name: Unzip goals
         run: |
@@ -173,5 +186,6 @@ jobs:
       - name: Run Plotting Script
         run: |
           cp config.tiny.yaml config.yaml
-          ./run-on-container.sh
+          sed -i 's@upload: False@upload: True/g' config.yaml
+          uv tool run snakemake all --cores all --config nbatch=${{matrix.nbatch}} ibatch=${{matrix.ibatch}}
 

From 51a74a720bc40c2605de35f5d31e2cd78ff9b314 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 11:15:27 +0200
Subject: [PATCH 18/30] chore: lake build before cache lake

---
 .github/workflows/cluster-scale-multi-width-ns.yml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/.github/workflows/cluster-scale-multi-width-ns.yml b/.github/workflows/cluster-scale-multi-width-ns.yml
index 2387995a8b..1c94560b98 100644
--- a/.github/workflows/cluster-scale-multi-width-ns.yml
+++ b/.github/workflows/cluster-scale-multi-width-ns.yml
@@ -70,6 +70,9 @@ jobs:
       - name: Make lake available
         run: |
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Lake Build
+        run: |
           pushd leanharness; lake build; popd
 
       - name: Cache lake.
@@ -167,6 +170,9 @@ jobs:
       - name: Make lake available
         run: |
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Lake Build
+        run: |
           pushd leanharness; lake build; popd
 
       - name: Cache lake.

From a7524490bf5c88919ae45defe2a1d37da6c83013 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 11:18:59 +0200
Subject: [PATCH 19/30] chore: run lake cache before calling lake build, d'oh

---
 .../cluster-scale-multi-width-ns.yml          | 31 ++++++++++---------
 1 file changed, 17 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/cluster-scale-multi-width-ns.yml b/.github/workflows/cluster-scale-multi-width-ns.yml
index 1c94560b98..57edaa45e1 100644
--- a/.github/workflows/cluster-scale-multi-width-ns.yml
+++ b/.github/workflows/cluster-scale-multi-width-ns.yml
@@ -71,10 +71,6 @@ jobs:
         run: |
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      - name: Lake Build
-        run: |
-          pushd leanharness; lake build; popd
-
       - name: Cache lake.
         id: cache-lake
         uses: actions/cache@v4
@@ -85,6 +81,10 @@ jobs:
           restore-keys: |
             ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
 
+      - name: Lake Build
+        run: |
+          pushd leanharness; lake build; popd
+
       - name: Unzip goals
         run: |
           unzip -o goals.zip
@@ -167,14 +167,6 @@ jobs:
           set -o pipefail
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
 
-      - name: Make lake available
-        run: |
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Lake Build
-        run: |
-          pushd leanharness; lake build; popd
-
       - name: Cache lake.
         id: cache-lake
         uses: actions/cache@v4
@@ -184,6 +176,15 @@ jobs:
           key: ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
           restore-keys: |
             ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
+            
+      - name: Make lake available
+        run: |
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Lake Build
+        run: |
+          pushd leanharness; lake build; popd
+
 
       - name: Unzip goals
         run: |
@@ -193,5 +194,7 @@ jobs:
         run: |
           cp config.tiny.yaml config.yaml
           sed -i 's@upload: False@upload: True/g' config.yaml
-          uv tool run snakemake all --cores all --config nbatch=${{matrix.nbatch}} ibatch=${{matrix.ibatch}}
-
+          # only allow rules to collate 'jsonl' and to plot.
+          uv tool run snakemake all --cores all \
+            --config nbatch=${{matrix.nbatch}} ibatch=${{matrix.ibatch}} \
+            --allowed-rules plot epoch_jsonl --cores all

From 72701bc9910a779f26b6bd045edcf853cd768211 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 11:27:35 +0200
Subject: [PATCH 20/30] chore: cache venv, fix sed

---
 .../cluster-scale-multi-width-ns.yml          | 23 ++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/cluster-scale-multi-width-ns.yml b/.github/workflows/cluster-scale-multi-width-ns.yml
index 57edaa45e1..7c973dd720 100644
--- a/.github/workflows/cluster-scale-multi-width-ns.yml
+++ b/.github/workflows/cluster-scale-multi-width-ns.yml
@@ -89,6 +89,16 @@ jobs:
         run: |
           unzip -o goals.zip
 
+      - name: Cache Venv
+        id: cache-venv
+        uses: actions/cache@v4
+        with:
+          path: |
+            .venv
+          key: ${{ runner.os }}-venv-${{ hashFiles('uv.lock', 'pyproject.toml') }}
+          restore-keys: |
+            ${{ runner.os }}-venv-${{ hashFiles('uv.lock', 'pyproject.toml') }}
+
       - name: Run Minibatch
         run: |
           ls
@@ -190,10 +200,21 @@ jobs:
         run: |
           unzip -o goals.zip
 
+      - name: Cache Venv
+        id: cache-venv
+        uses: actions/cache@v4
+        with:
+          path: |
+            .venv
+          key: ${{ runner.os }}-venv-${{ hashFiles('uv.lock', 'pyproject.toml') }}
+          restore-keys: |
+            ${{ runner.os }}-venv-${{ hashFiles('uv.lock', 'pyproject.toml') }}
+
+
       - name: Run Plotting Script
         run: |
           cp config.tiny.yaml config.yaml
-          sed -i 's@upload: False@upload: True/g' config.yaml
+          sed -i 's@upload: False@upload: True@g' config.yaml
           # only allow rules to collate 'jsonl' and to plot.
           uv tool run snakemake all --cores all \
             --config nbatch=${{matrix.nbatch}} ibatch=${{matrix.ibatch}} \

From 2762848253637f7ad37889f605753ef94c9f23d6 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 11:34:06 +0200
Subject: [PATCH 21/30] chore: fix upload

---
 .github/workflows/cluster-scale-multi-width-ns.yml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/cluster-scale-multi-width-ns.yml b/.github/workflows/cluster-scale-multi-width-ns.yml
index 7c973dd720..005648e947 100644
--- a/.github/workflows/cluster-scale-multi-width-ns.yml
+++ b/.github/workflows/cluster-scale-multi-width-ns.yml
@@ -140,8 +140,8 @@ jobs:
           ref: "master"
           token: ${{ secrets.NSCLOUD_GITHUB_TOKEN }}
 
-      - name: Download data
-        uses: actions/download-artifact@v5
+      - name: Download Data From Artifact
+        uses: namespace-actions/download-artifact@v5
         with:
           path: autogenerated/
           pattern: ${{ github.run_id }}-ibatch-*
@@ -217,5 +217,4 @@ jobs:
           sed -i 's@upload: False@upload: True@g' config.yaml
           # only allow rules to collate 'jsonl' and to plot.
           uv tool run snakemake all --cores all \
-            --config nbatch=${{matrix.nbatch}} ibatch=${{matrix.ibatch}} \
             --allowed-rules plot epoch_jsonl --cores all

From c2721fe368f49407f2fc367435ced4edda7e7dc9 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 11:37:00 +0200
Subject: [PATCH 22/30] chore: fix version of download action

---
 .github/workflows/cluster-scale-multi-width-ns.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/cluster-scale-multi-width-ns.yml b/.github/workflows/cluster-scale-multi-width-ns.yml
index 005648e947..52a27c01be 100644
--- a/.github/workflows/cluster-scale-multi-width-ns.yml
+++ b/.github/workflows/cluster-scale-multi-width-ns.yml
@@ -141,7 +141,7 @@ jobs:
           token: ${{ secrets.NSCLOUD_GITHUB_TOKEN }}
 
       - name: Download Data From Artifact
-        uses: namespace-actions/download-artifact@v5
+        uses: namespace-actions/download-artifact@v1
         with:
           path: autogenerated/
           pattern: ${{ github.run_id }}-ibatch-*

From 45e2bfcf10b6323499f22ef1229a1e2b37851584 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 11:41:05 +0200
Subject: [PATCH 23/30] chore: gotta figure paths out

---
 .github/workflows/cluster-scale-multi-width-ns.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/cluster-scale-multi-width-ns.yml b/.github/workflows/cluster-scale-multi-width-ns.yml
index 52a27c01be..df8aa4c708 100644
--- a/.github/workflows/cluster-scale-multi-width-ns.yml
+++ b/.github/workflows/cluster-scale-multi-width-ns.yml
@@ -213,6 +213,9 @@ jobs:
 
       - name: Run Plotting Script
         run: |
+          ls
+          ls autogenerated/
+          find autogenerated/ 
           cp config.tiny.yaml config.yaml
           sed -i 's@upload: False@upload: True@g' config.yaml
           # only allow rules to collate 'jsonl' and to plot.

From c2ad308c25e84fca5e95c0248e15fe5b448d89a2 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 11:46:21 +0200
Subject: [PATCH 24/30] chore: pass nbatch

---
 .github/workflows/cluster-scale-multi-width-ns.yml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/cluster-scale-multi-width-ns.yml b/.github/workflows/cluster-scale-multi-width-ns.yml
index df8aa4c708..fac4637e95 100644
--- a/.github/workflows/cluster-scale-multi-width-ns.yml
+++ b/.github/workflows/cluster-scale-multi-width-ns.yml
@@ -129,6 +129,10 @@ jobs:
       - nscloud-git-mirror-5gb
       - nscloud-container-image-cache
       - nscloud-runner-tool-cache-20gb
+    strategy:
+      matrix:
+        nbatch: [3]
+
     steps:
       - name: Setup Ephemeral NS Cluster
         uses: namespacelabs/nscloud-setup@v0
@@ -213,11 +217,11 @@ jobs:
 
       - name: Run Plotting Script
         run: |
-          ls
-          ls autogenerated/
           find autogenerated/ 
+
           cp config.tiny.yaml config.yaml
           sed -i 's@upload: False@upload: True@g' config.yaml
           # only allow rules to collate 'jsonl' and to plot.
           uv tool run snakemake all --cores all \
+            --config nbatch=${{matrix.nbatch}} \
             --allowed-rules plot epoch_jsonl --cores all

From ad783ae70e57add210ce355eeba5c0547b69b060 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 11:52:48 +0200
Subject: [PATCH 25/30] chore: switch to using full config, not tiny config

---
 .github/workflows/cluster-scale-multi-width-ns.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/cluster-scale-multi-width-ns.yml b/.github/workflows/cluster-scale-multi-width-ns.yml
index fac4637e95..f03e0240e6 100644
--- a/.github/workflows/cluster-scale-multi-width-ns.yml
+++ b/.github/workflows/cluster-scale-multi-width-ns.yml
@@ -105,7 +105,7 @@ jobs:
           pwd
           set -o pipefail
           curl -LsSf https://astral.sh/uv/install.sh | sh
-          cp config.tiny.yaml config.yaml
+          cp config.full.yaml config.yaml
           uv tool run snakemake run_minibatch --cores all --config nbatch=${{matrix.nbatch}} ibatch=${{matrix.ibatch}}
 
       - name: Upload Data As Artifact
@@ -219,7 +219,7 @@ jobs:
         run: |
           find autogenerated/ 
 
-          cp config.tiny.yaml config.yaml
+          cp config.full.yaml config.yaml
           sed -i 's@upload: False@upload: True@g' config.yaml
           # only allow rules to collate 'jsonl' and to plot.
           uv tool run snakemake all --cores all \

From 73c642619c38390505b7ee0cbe4fb2d345175648 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 26 Sep 2025 14:13:03 +0200
Subject: [PATCH 26/30] chore: add comment on how this can be improved

---
 .github/workflows/cluster-scale-multi-width-ns.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/cluster-scale-multi-width-ns.yml b/.github/workflows/cluster-scale-multi-width-ns.yml
index f03e0240e6..5ebf21424b 100644
--- a/.github/workflows/cluster-scale-multi-width-ns.yml
+++ b/.github/workflows/cluster-scale-multi-width-ns.yml
@@ -1,3 +1,6 @@
+# This can be improved by building a docker image of the deps:
+# https://github.com/opencompl/lean-mlir/blob/0048c677755a4544b8e35904549f20d8b48939de/.github/workflows/docker.yml
+# and then running once with that image.
 name: +++ Cluster-Scale Multi-Width (NS) +++
 on:
   push:

From 06076a92d4623b0b12eab27a7e7042dc8eb9023d Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 7 Oct 2025 23:33:54 +0100
Subject: [PATCH 27/30] chore: update runner

---
 .github/workflows/cluster-scale-multi-width-ns.yml | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/cluster-scale-multi-width-ns.yml b/.github/workflows/cluster-scale-multi-width-ns.yml
index 5ebf21424b..9ed331683b 100644
--- a/.github/workflows/cluster-scale-multi-width-ns.yml
+++ b/.github/workflows/cluster-scale-multi-width-ns.yml
@@ -1,12 +1,12 @@
 # This can be improved by building a docker image of the deps:
 # https://github.com/opencompl/lean-mlir/blob/0048c677755a4544b8e35904549f20d8b48939de/.github/workflows/docker.yml
 # and then running once with that image.
-name: +++ Cluster-Scale Multi-Width (NS) +++
+name: Cluster-Scale Multi-Width (NS) 
+
+
 on:
-  push:
-    branches:
-      - "main"
-  pull_request:
+  issue_comment:
+    types: [created]
 
 permissions:
   contents: write
@@ -14,6 +14,10 @@ permissions:
 
 jobs:
   run-batch:
+    if: >
+      github.event.issue.pull_request != null &&
+      startsWith(github.event.comment.body, '!blase')
+
     name: Batch Run
     runs-on:
       - nscloud-ubuntu-24.04-amd64-16x32-with-cache

From f0c779576a8f09646599b753277cef938dc60127 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 7 Oct 2025 23:34:56 +0100
Subject: [PATCH 28/30] chore: bring back stuff

---
 .github/workflows/automerge.yml              |  31 +++
 .github/workflows/doc.yml                    |  43 ++++
 .github/workflows/docker.yml                 | 228 +++++++++++++++++++
 .github/workflows/elan-gc.yml                |  10 +
 .github/workflows/medusa.yml                 |  56 +++++
 .github/workflows/update-mathlib-version.yml |  69 ++++++
 6 files changed, 437 insertions(+)
 create mode 100644 .github/workflows/automerge.yml
 create mode 100644 .github/workflows/doc.yml
 create mode 100644 .github/workflows/docker.yml
 create mode 100644 .github/workflows/elan-gc.yml
 create mode 100644 .github/workflows/medusa.yml
 create mode 100644 .github/workflows/update-mathlib-version.yml

diff --git a/.github/workflows/automerge.yml b/.github/workflows/automerge.yml
new file mode 100644
index 0000000000..c69cb3f7b0
--- /dev/null
+++ b/.github/workflows/automerge.yml
@@ -0,0 +1,31 @@
+name: automerge
+on:
+  pull_request:
+    types:
+      - labeled
+      - unlabeled
+      - synchronize
+      - opened
+      - edited
+      - ready_for_review
+      - reopened
+      - unlocked
+  pull_request_review:
+    types:
+      - submitted
+  check_suite:
+    types:
+      - completed
+  status: {}
+jobs:
+  automerge:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+      pull-requests: write
+    steps:
+      - id: automerge
+        name: automerge
+        uses: "pascalgn/automerge-action@v0.16.4"
+        env:
+          GITHUB_TOKEN: "${{ secrets.GITHUB_TOKEN }}"
diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml
new file mode 100644
index 0000000000..62d7b9efac
--- /dev/null
+++ b/.github/workflows/doc.yml
@@ -0,0 +1,43 @@
+name: docs
+on:
+  push:
+    branches:
+      - "main-disabled"
+
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+jobs:
+  build:
+    name: build and deploy documentation.
+    # Exclude expensive self-hosted runner. Reserved for performance benchmarking.
+    # https://docs.github.com/en/enterprise-cloud@latest/actions/writing-workflows/choosing-where-your-workflow-runs/choosing-the-runner-for-a-job#choosing-github-hosted-runners
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout 🛎️
+        uses: actions/checkout@v3
+
+      - name: Install elan 🕑
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+  
+      - name: Generate docs 📜
+        run: |
+          ./docgen.sh
+
+# stolen from mathlib: https://github.com/leanprover-community/mathlib4_docs/blob/1f4ea7657bc377b4298fd400e567471d3a248b2d/.github/workflows/docs.yaml#L79-L86
+      - name: Upload artifact 📁
+        uses: actions/upload-pages-artifact@v1
+        with:
+          path: '.lake/build/doc'
+
+      - name: Deploy to GitHub Pages 🚀
+        id: deployment
+        uses: actions/deploy-pages@v1
+
diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
new file mode 100644
index 0000000000..e5aecf29e9
--- /dev/null
+++ b/.github/workflows/docker.yml
@@ -0,0 +1,228 @@
+name: Build & Evaluate (in Docker)
+on:
+  workflow_dispatch:
+  push:
+   branches:
+     - "main"
+  pull_request:
+  merge_group:
+
+# ^^ This workflow does not run automatically, to make sure we don't burn through too many
+# namespace.so credits. For now, it is only triggered manually if desired.
+
+permissions:
+  contents: write
+  packages: write
+
+jobs:
+  #
+  # Docker image builders
+  #
+  core-docker-img:
+    name: Build Docker image for core library
+    runs-on: namespace-profile-leanmlir-docker-cached
+    steps:
+      - name: Login to GitHub Container Registry
+        uses: docker/login-action@v3
+        with:
+          registry: ghcr.io
+          username: ${{ github.repository_owner }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Checkout 🛎️
+        uses: actions/checkout@v3
+
+      - name: Setup Docker metadata
+        id: meta
+        uses: docker/metadata-action@v5
+        with:
+          images: |
+            ghcr.io/opencompl/lean-mlir
+            nscr.io/2411cf8f8l302/lean-mlir
+          tags: |
+            type=ref,event=branch
+            type=ref,event=pr
+            type=raw,value=${{ github.sha }}
+            type=raw,value=latest,enable={{is_default_branch}}
+
+      - name: Build and push
+        uses: docker/build-push-action@v6
+        with:
+          context: .
+          push: true
+          tags: ${{ steps.meta.outputs.tags }}
+          labels: ${{ steps.meta.outputs.labels }}
+
+#   instcombine-docker-img:
+#     name: Build Docker image for InstCombine Evaluation
+#     runs-on: ubuntu-latest # Run on GH-provided runner
+#     needs: core-docker-img
+#     steps:
+#       - name: Set up Docker Buildx
+#         uses: docker/setup-buildx-action@v3
+#
+#       - name: Login to GitHub Container Registry
+#         uses: docker/login-action@v3
+#         with:
+#           registry: ghcr.io
+#           username: ${{ github.repository_owner }}
+#           password: ${{ secrets.GITHUB_TOKEN }}
+#
+#       - name: Checkout 🛎️
+#         uses: actions/checkout@v3
+#
+#       - name: Setup Docker metadata
+#         id: meta
+#         uses: docker/metadata-action@v5
+#         with:
+#           images: ghcr.io/opencompl/lean-mlir-instcombine
+#           tags: |
+#             type=ref,event=branch
+#             type=ref,event=pr
+#             type=raw,value=${{ github.sha }}
+#             type=raw,value=latest,enable={{is_default_branch}}
+#
+#       - name: Build and push Docker image
+#         uses: docker/build-push-action@v6
+#         with:
+#           context: "./bv-evaluation"
+#           build-args: |
+#             LEANMLIR_TAG=${{ github.sha }}
+#           push: true
+#           tags: ${{ steps.meta.outputs.tags }}
+#           labels: ${{ steps.meta.outputs.labels }}
+#           cache-from: type=gha
+#           cache-to: type=gha,mode=max
+
+  #
+  # Evaluation & test jobs
+  #
+  build-tools:
+    name: use docker (runs on namespace)
+    runs-on: namespace-profile-leanmlir-small
+    needs: core-docker-img
+    container: "nscr.io/2411cf8f8l302/lean-mlir:${{ github.sha }}"
+    defaults:
+      run:
+        working-directory: /code/lean-mlir
+    steps:
+      - name: Symlink .elan (to correct for GHA changing $HOME)
+        run: '[ -e ~/.elan ] || ln -s /root/.elan ~/.elan'
+      - name: Run lake build
+        run: |
+          lake -R build
+
+  build-tools-ghcr:
+    name: use docker (runs on namespace, via ghcr.io)
+    runs-on: namespace-profile-leanmlir-small
+    needs: core-docker-img
+    container: "ghcr.io/opencompl/lean-mlir:${{ github.sha }}"
+    defaults:
+      run:
+        working-directory: /code/lean-mlir
+    steps:
+      - name: Symlink .elan (to correct for GHA changing $HOME)
+        run: '[ -e ~/.elan ] || ln -s /root/.elan ~/.elan'
+      - name: Run lake build
+        run: |
+          lake -R build
+
+  build-tools-github:
+    name: use docker (runs on GitHub)
+    runs-on: ubuntu-latest # Run on GH-provided runner
+    needs: core-docker-img
+    container: "ghcr.io/opencompl/lean-mlir:${{ github.sha }}"
+    defaults:
+      run:
+        working-directory: /code/lean-mlir
+    steps:
+      - name: Symlink .elan (to correct for GHA changing $HOME)
+        run: '[ -e ~/.elan ] || ln -s /root/.elan ~/.elan'
+      - name: Run lake build
+        run: |
+          lake -R build
+
+#   alive-check-changes:
+#     name: Check for changes in AliveStatements
+#     runs-on: ubuntu-latest # Run on GH-provided runner
+#     needs: instcombine-docker-img
+#     container: "ghcr.io/opencompl/lean-mlir-instcombine:${{ github.sha }}"
+#     defaults:
+#       run:
+#         working-directory: /code/lean-mlir
+#     steps:
+#       - name: Symlink .elan (to correct for GHA changing $HOME)
+#         run: '[ -e ~/.elan ] || ln -s /root/.elan ~/.elan'
+#
+#       - run: |
+#           lake build AliveExamples
+#           (cd SSA/Projects/InstCombine/; uv run ./update_alive_statements.py)
+#           # /--------------------------- ^^^^^^
+#           # | TODO: this could be removed if we add a uv shebang to the python file
+#           bash -c '! git diff -- SSA/Projects/InstCombine | grep .'  # iff git diff is empty, 'grep .' fails, '!' inverts the failure, and in the forced bash
+#
+#   evaluation-LLVM:
+#     name: Evaluate LLVM
+#     runs-on: ubuntu-latest # Run on GH-provided runner
+#     needs: instcombine-docker-img
+#     container: "ghcr.io/opencompl/lean-mlir-instcombine:${{ github.sha }}"
+#     defaults:
+#       run:
+#         working-directory: /code/lean-mlir/bv-evaluation
+#     permissions:
+#       pull-requests: write
+#     steps:
+#       - name: Symlink .elan (to correct for GHA changing $HOME)
+#         run: '[ -e ~/.elan ] || ln -s /root/.elan ~/.elan'
+#
+#       - name: Run LLVM
+#         continue-on-error: true
+#         run: |
+#           uv run ./compare.py instcombine -j48 \
+#             || (echo "LEANMLIR_STATUS=fail" >> $GITHUB_ENV; exit 1)
+#
+#       - name: Collect data LLVM
+#         continue-on-error: true
+#         run: |
+#           (uv run ./collect.py instcombine | tee llvm-stats) \
+#             || (echo "LEANMLIR_STATUS=fail" >> $GITHUB_ENV; exit 1)
+#
+#       - uses: actions/github-script@v6
+#         if: env.LEANMLIR_STATUS != 'fail' && github.event_name == 'pull_request'
+#         with:
+#           script: |
+#             const fs = require('fs')
+#             github.rest.issues.createComment({
+#               issue_number: context.issue.number,
+#               owner: context.repo.owner,
+#               repo: context.repo.repo,
+#               body: fs.readFileSync('/code/lean-mlir/bv-evaluation/llvm-stats', 'utf8')
+#             })
+#
+#       - name: Upload LLVM artifact
+#         uses: actions/upload-artifact@v4
+#         with:
+#           name: LLVM evaluation
+#           path: results
+#
+#   extract-goals:
+#     name: Extract goals
+#     runs-on: ubuntu-latest # Run on GH-provided runner
+#     needs: instcombine-docker-img
+#     container: "ghcr.io/opencompl/lean-mlir-instcombine:${{ github.sha }}"
+#     defaults:
+#       run:
+#         working-directory: /code/lean-mlir
+#     strategy:
+#       matrix:
+#         extract_offset: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
+#         extract_stride: [10]
+#     steps:
+#       - name: Symlink .elan (to correct for GHA changing $HOME)
+#         run: '[ -e ~/.elan ] || ln -s /root/.elan ~/.elan'
+#
+#       - name: Ensure InstCombine goals are up-to-date
+#         env:
+#           GIT_DIR: ${{ github.workspace }}/.git
+#         run: |
+#           bash SSA/Projects/InstCombine/scripts/test-extract-goals.sh --nfiles 9000 -j7  --stride ${{matrix.extract_stride}} --offset ${{matrix.extract_offset}}
diff --git a/.github/workflows/elan-gc.yml b/.github/workflows/elan-gc.yml
new file mode 100644
index 0000000000..4672b1aa7d
--- /dev/null
+++ b/.github/workflows/elan-gc.yml
@@ -0,0 +1,10 @@
+name: Garbage collect elan toolchains
+on:
+  schedule:
+    - cron: '0 9 * * 1' # Run weekly, at 09:00 on Monday
+
+jobs:
+  elan-gc:
+    runs-on: self-hosted
+    steps:
+      - run: elan toolchain gc --delete
diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml
new file mode 100644
index 0000000000..e581b66aeb
--- /dev/null
+++ b/.github/workflows/medusa.yml
@@ -0,0 +1,56 @@
+name: Medusa Build & Test
+on:
+  push:
+    branches:
+      - "main"
+    paths:
+      - 'Medusa/**'
+  pull_request:
+    paths:
+      - 'Medusa/**'
+
+  merge_group:
+
+permissions:
+  contents: write
+  packages: write
+
+jobs:
+  build:
+    name: medusa
+    permissions:
+      pull-requests: write
+    # Exclude expensive self-hosted runner. Reserved for performance benchmarking.
+    # https://docs.github.com/en/enterprise-cloud@latest/actions/writing-workflows/choosing-where-your-workflow-runs/choosing-the-runner-for-a-job#choosing-github-hosted-runners
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout 🛎️
+        uses: actions/checkout@v3
+
+      - name: Install elan 🕑
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Cache `.lake` folder
+        id: cache-lake
+        uses: actions/cache@v4
+        with:
+          path: Medusa/.lake
+          key: ${{ runner.os }}-lake-${{ hashFiles('Medusa/lake-manifest.json') }}-4
+
+      - name: Get mathlib cache (only if no cache available)
+        if: steps.cache-lake.outputs.cache-hit != 'true'
+        continue-on-error: true
+        run: |
+          (pushd Medusa; lake -R exe cache get; true; popd) # download cache of mathlib docs.
+
+      - name: Compile Medusa
+        run: |
+          pushd Medusa; lake -R build Medusa --iofail
+
+      - name: Test Medusa
+        run: |
+          pushd Medusa; lake test; popd
diff --git a/.github/workflows/update-mathlib-version.yml b/.github/workflows/update-mathlib-version.yml
new file mode 100644
index 0000000000..1b746c8e2e
--- /dev/null
+++ b/.github/workflows/update-mathlib-version.yml
@@ -0,0 +1,69 @@
+name: Update mathlib version
+on:
+  schedule:
+    - cron: '44 * * * *'
+  workflow_dispatch:
+
+permissions: write-all
+
+jobs:
+  mathlibtoday:
+    name: Update Mathlib & Lean
+    strategy:
+      fail-fast: false
+      matrix:
+        daysbefore: [0, 1, 2, 3, 4, 5, 6, 7, 8]
+    permissions: write-all
+    # Exclude expensive self-hosted runner. Reserved for performance benchmarking.
+    # https://docs.github.com/en/enterprise-cloud@latest/actions/writing-workflows/choosing-where-your-workflow-runs/choosing-the-runner-for-a-job#choosing-github-hosted-runners
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout 🛎️
+        uses: actions/checkout@v4
+        with:
+          token: ${{secrets.PAT}}
+
+      - name: Install elan 🕑
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Get Mathlib Date
+        id: mldate
+        run: |
+           echo "date=`date -d '-${{matrix.daysbefore}} day' +20%y-%m-%d`"
+           echo "date=`date -d '-${{matrix.daysbefore}} day' +20%y-%m-%d`" >> $GITHUB_OUTPUT
+
+      - name: install zsh
+        run: |
+          sudo apt-get update; sudo apt-get install zsh
+
+      - name: Check if lean toolchain is already newer or equally old
+        shell: zsh {0}
+        run: |
+           if [[ `cat lean-toolchain | sed -e 's/leanprover\/lean4:nightly-//' | sed -e '/$^/d' | sed -e 's/-//g' ` -ge `echo ${{steps.mldate.outputs.date}} | sed -e 's/-//g'` ]]; then echo "abort: lean-toolchain is newer than proposed date"; false ; fi
+
+      - name: Set Mathlib Date
+        run: |
+           sed -e "s/\"nightly-testing.*\"/\"nightly-testing-${{steps.mldate.outputs.date}}\"/" -i lakefile.toml
+           sed -e "s/nightly.*/nightly-${{steps.mldate.outputs.date}}/" -i lean-toolchain
+           echo "## lakefile.toml"
+           cat lakefile.toml
+           echo "## lean-toolchain"
+           cat lean-toolchain
+           lake update mathlib
+
+      - name: Merge pre-existing pull request
+        continue-on-error: true
+        run: |
+           git merge origin/auto-mathlib-update-${{steps.mldate.outputs.date}}
+
+      - name: Create Pull Request
+        uses: peter-evans/create-pull-request@v7
+        with:
+          title: "${{steps.mldate.outputs.date}} lean nightly update"
+          branch: "auto-mathlib-update-${{steps.mldate.outputs.date}}"
+          body: "automatic update of mathlib + lean via GitHub action."
+          token: ${{secrets.PAT}}

From a8169bce0d57690981d8e87893243b923161113b Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 7 Oct 2025 23:42:32 +0100
Subject: [PATCH 29/30] chore: add cluster runner

---
 .github/workflows/cluster-scale-multi-width-ns.yml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/cluster-scale-multi-width-ns.yml b/.github/workflows/cluster-scale-multi-width-ns.yml
index 9ed331683b..4bcb7f04d2 100644
--- a/.github/workflows/cluster-scale-multi-width-ns.yml
+++ b/.github/workflows/cluster-scale-multi-width-ns.yml
@@ -1,7 +1,7 @@
 # This can be improved by building a docker image of the deps:
 # https://github.com/opencompl/lean-mlir/blob/0048c677755a4544b8e35904549f20d8b48939de/.github/workflows/docker.yml
 # and then running once with that image.
-name: Cluster-Scale Multi-Width (NS) 
+name: YYY Cluster-Scale Multi-Width (NS)  YYY
 
 
 on:
@@ -14,9 +14,7 @@ permissions:
 
 jobs:
   run-batch:
-    if: >
-      github.event.issue.pull_request != null &&
-      startsWith(github.event.comment.body, '!blase')
+    if: github.event.issue.pull_request != null && startsWith(github.event.comment.body, "!blase")
 
     name: Batch Run
     runs-on:

From 771292e0c44ecbba3ad6ffc34c57e99ad52785b5 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 8 Oct 2025 16:44:38 +0100
Subject: [PATCH 30/30] chore: add abstracter

---
 Blase/README.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Blase/README.md b/Blase/README.md
index e59bba5994..6b5ec3fe49 100644
--- a/Blase/README.md
+++ b/Blase/README.md
@@ -16,6 +16,8 @@ For stable releases, please change the `rev` to the desired version tag.
 
 #### Algorithms Improvements TODO
 
+- [ ] Write a tactic that takes a goal state with BVs and generalizes them to an arbitrary width. 
+      Call this `bv_abstract`.
 - [ ] Add evaluation from Sam Coward.
 - [ ] Add evaluation from Lean's bitvector suite.
 - [ ] Add right shift and division support by eliminating into left-shift and multiplication.