From 4fad46060ce75625bb1ce9b8f7d43d1b14eee011 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Thu, 20 Aug 2026 13:00:28 -0400
Subject: [PATCH 1/3] fix: doc-gen4 deps

This fixes the dependency ordering between mathlib and doc-gen4 so that mathlib cache works, and has the results of running lake update with '-Kenv=doc' so that the static site generator action can work
---
 lake-manifest.json | 52 +++++++++++++++++++++++++++++++++++++++++++++-
 lakefile.lean      |  9 ++++----
 2 files changed, 56 insertions(+), 5 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 7e171695..0424cb1c 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -11,6 +11,16 @@
    "inputRev": "v4.29.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "aa4c3e4e14f5b31495b7c7238762ecceddd9f52c",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
@@ -90,6 +100,46 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "v4.29.0",
    "inherited": true,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/kim-em/leansqlite",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "d14544c72b593af6a66131bc34cdab16bf7c0940",
+   "name": "leansqlite",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "suppress-reducibility-warning",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "9539e34e5cb2d52a6454d9b6218f6b6835cad071",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly-testing",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"}],
  "name": "sampcert",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 0dded9f6..212994f9 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,12 +4,13 @@ open Lake DSL System
 package «sampcert» where
   testDriver := "test"
 
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "v4.29.0"
-
 -- From doc-gen4
 meta if get_config? env = some "doc" then
-require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
+require «doc-gen4» from git
+  "https://github.com/leanprover/doc-gen4" @ "v4.29.0"
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.29.0"
 
 target ffi.o (pkg : NPackage __name__) : FilePath := do
   let oFile := pkg.buildDir / "ffi.o"

From fe5fd55283b60571dc4b13fc1c1366bd3b856028 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Thu, 20 Aug 2026 13:01:33 -0400
Subject: [PATCH 2/3] Just unconditionally require doc-gen4

---
 lakefile.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index 212994f9..c9d46428 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,8 +4,6 @@ open Lake DSL System
 package «sampcert» where
   testDriver := "test"
 
--- From doc-gen4
-meta if get_config? env = some "doc" then
 require «doc-gen4» from git
   "https://github.com/leanprover/doc-gen4" @ "v4.29.0"
 

From 66477b1403be726f4adca66a8bed6c9a929646f9 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Thu, 20 Aug 2026 13:03:36 -0400
Subject: [PATCH 3/3] Remove -R -Kenv=doc references

---
 .github/workflows/static.yml | 4 ++--
 CONTRIBUTING.md              | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/static.yml b/.github/workflows/static.yml
index 3253a76f..1b1d82d7 100644
--- a/.github/workflows/static.yml
+++ b/.github/workflows/static.yml
@@ -32,11 +32,11 @@ jobs:
       - uses: leanprover/lean-action@v1
         with:
           test: false
-          build-args: "-R -Kwerror -Kenv=doc" # IDK if these are necessary?
+          build-args: "-Kwerror"
           use-mathlib-cache: true
       - name: build docs
         run: |
-          lake build -R -Kwerror -Kenv=doc SampCert:docs
+          lake build -Kwerror SampCert:docs
       - name: Upload artifact
         uses: actions/upload-pages-artifact@v3
         with:
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 69352afb..651bd7c2 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -17,7 +17,7 @@ Barring the exceptions made for extraction, SLang programs should follow this na
 
 ## Tools
 
-SampCert uses [doc-gen4](https://github.com/leanprover/doc-gen4) to render its documentation. You can build a local copy using the command ``lake -R -Kenv=doc build SampCert:docs``.
+SampCert uses [doc-gen4](https://github.com/leanprover/doc-gen4) to render its documentation. You can build a local copy using the command ``lake build SampCert:docs``.
 
 SampCert also installs [import-graph](https://github.com/leanprover-community/import-graph). The command ``lake exe graph --to SampCert import_graph.pdf`` will render a dependency graph between SampCert files.