From 6e018b49bdc4e128362c7feb65675f40abd365ce Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 22 Oct 2025 10:37:25 +0100
Subject: [PATCH 1/5] Update build.yml

---
 .github/workflows/build.yml | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index b3e044c2e..49911c0b3 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -41,6 +41,14 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
+      - name: runLinter on PhysLean
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
+        id: lint
+        uses: liskin/gh-problem-matcher-wrap@v3
+        with:
+          linters: gcc
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter PhysLean
+
       - name: check file imports
         run: |
           bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports"
@@ -53,13 +61,6 @@ jobs:
         run: |
           bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe sorry_lint"
 
-      - name: runLinter on PhysLean
-        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
-        id: lint
-        uses: liskin/gh-problem-matcher-wrap@v3
-        with:
-          linters: gcc
-          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter PhysLean
 
   style_lint:
     name: Python based style linter

From a5c62d972b4bebd8e019c5e53e4986553fa24def Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 22 Oct 2025 11:05:49 +0100
Subject: [PATCH 2/5] simplification of build step

---
 .github/workflows/build.yml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 49911c0b3..0a2145f63 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -42,12 +42,8 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
       - name: runLinter on PhysLean
-        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
-        id: lint
-        uses: liskin/gh-problem-matcher-wrap@v3
-        with:
-          linters: gcc
-          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter PhysLean
+        run: |
+          env LEAN_ABORT_ON_PANIC=1 lake exe runLinter PhysLean
 
       - name: check file imports
         run: |

From 16e0cb52808a0967ccfbf6aae8b820c6364cd9f4 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 22 Oct 2025 11:34:47 +0100
Subject: [PATCH 3/5] extreme simplification

---
 .github/workflows/build.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 0a2145f63..b2010c716 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -43,7 +43,7 @@ jobs:
 
       - name: runLinter on PhysLean
         run: |
-          env LEAN_ABORT_ON_PANIC=1 lake exe runLinter PhysLean
+          lake exe runLinter PhysLean
 
       - name: check file imports
         run: |

From bcfcd7650ff43d3cb556bbe05545082f86cc1848 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 22 Oct 2025 13:20:26 +0100
Subject: [PATCH 4/5] track elan version

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

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index b2010c716..f229b3e19 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -28,6 +28,7 @@ jobs:
         run: |
           lean --version
           lake --version
+          elan --version
 
       - name: build cache
         run: |
@@ -43,7 +44,7 @@ jobs:
 
       - name: runLinter on PhysLean
         run: |
-          lake exe runLinter PhysLean
+          env LEAN_ABORT_ON_PANIC=1 lake exe runLinter PhysLean
 
       - name: check file imports
         run: |

From f2e2935e3adb317b43c01f2aa4a3ec7dc45caff6 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 22 Oct 2025 13:32:39 +0100
Subject: [PATCH 5/5] Create BuildArtifact.yml

---
 .github/workflows/BuildArtifact.yml | 53 +++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)
 create mode 100644 .github/workflows/BuildArtifact.yml

diff --git a/.github/workflows/BuildArtifact.yml b/.github/workflows/BuildArtifact.yml
new file mode 100644
index 000000000..8d9b54383
--- /dev/null
+++ b/.github/workflows/BuildArtifact.yml
@@ -0,0 +1,53 @@
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - master
+
+name: Style linters
+
+jobs:
+  doc_lint:
+    name: Lean based style linters
+    runs-on: ubuntu-latest
+    steps:
+
+      - uses: actions/checkout@v4
+
+      - 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: check versions
+        run: |
+          lean --version
+          lake --version
+          elan --version
+
+      - name: build cache
+        run: |
+          lake exe cache get
+
+      - name: build PhysLean
+        id: build
+        uses: liskin/gh-problem-matcher-wrap@v3
+        with:
+          linters: gcc
+          run: |
+            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
+      - name: copy build data
+        run: |
+          mv .lake lake-artifact/.lake
+
+      - name: Upload build artifact
+        uses: actions/upload-artifact@v4
+        with:
+          name: lake
+          path: lake-artifact/
+          retention-days: 90