From c17127834cbd5392eb1eb3fe5e45d3641b6a0369 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 18:24:44 -0700
Subject: [PATCH 1/2] ci: reproduce A263135 documentation failure

---
 .github/workflows/a263135-docs-repro.yml | 76 ++++++++++++++++++++++++
 1 file changed, 76 insertions(+)
 create mode 100644 .github/workflows/a263135-docs-repro.yml

diff --git a/.github/workflows/a263135-docs-repro.yml b/.github/workflows/a263135-docs-repro.yml
new file mode 100644
index 00000000..4cb0e670
--- /dev/null
+++ b/.github/workflows/a263135-docs-repro.yml
@@ -0,0 +1,76 @@
+# Copyright 2026 Dominic Dabish
+# Licensed under the Apache License, Version 2.0.
+
+name: A263135 documentation reproduction
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/a263135-docs-repro.yml'
+      - 'audits/a263135-docs-repro.md'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  reproduce:
+    name: reproduce doc-gen failure
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    steps:
+      - name: Checkout exact A263135 PR head
+        uses: actions/checkout@v6
+        with:
+          repository: DomTheDeveloper/formal-conjectures
+          ref: 7f1bd9fd95a3718bb7e849620a9c96176aa0defc
+          fetch-depth: 1
+
+      - name: Record exact commit
+        run: git rev-parse HEAD | tee "$RUNNER_TEMP/resolved-sha.txt"
+
+      - name: Install repository-pinned Lean
+        run: |
+          set -euo pipefail
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Restore Mathlib cache
+        run: |
+          set -euo pipefail
+          "$HOME/.elan/bin/lake" exe cache unpack || true
+          "$HOME/.elan/bin/lake" exe cache get
+
+      - name: Build Lean project
+        run: |
+          set -o pipefail
+          : > "$RUNNER_TEMP/a263135-docs.log"
+          "$HOME/.elan/bin/lake" --wfail build \
+            2>&1 | tee "$RUNNER_TEMP/a263135-docs.log"
+
+      - name: Prepare documentation project
+        run: |
+          set -o pipefail
+          cd docbuild
+          export MATHLIB_NO_CACHE_ON_UPDATE=1
+          "$HOME/.elan/bin/lake" update formal_conjectures \
+            2>&1 | tee -a "$RUNNER_TEMP/a263135-docs.log"
+
+      - name: Build documentation
+        run: |
+          set -o pipefail
+          cd docbuild
+          "$HOME/.elan/bin/lake" build FormalConjectures:docs \
+            2>&1 | tee -a "$RUNNER_TEMP/a263135-docs.log"
+
+      - name: Upload complete reproduction log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: a263135-docs-repro-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/resolved-sha.txt
+            ${{ runner.temp }}/a263135-docs.log
+          if-no-files-found: warn

From aa4354269e0a4a6f89b9ff72e08dddfbee4fc096 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 18:24:52 -0700
Subject: [PATCH 2/2] docs: record A263135 docs reproduction

---
 audits/a263135-docs-repro.md | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 audits/a263135-docs-repro.md

diff --git a/audits/a263135-docs-repro.md b/audits/a263135-docs-repro.md
new file mode 100644
index 00000000..a23a7f2c
--- /dev/null
+++ b/audits/a263135-docs-repro.md
@@ -0,0 +1,8 @@
+# A263135 documentation reproduction
+
+This workflow checks the exact current upstream PR #4571 head
+`7f1bd9fd95a3718bb7e849620a9c96176aa0defc`.
+
+The upstream Lean compilation passed, but `FormalConjectures:docs` failed. This
+reproduction runs the same Lean and documentation stages and always uploads the
+complete combined log so the failure can be diagnosed without guessing.