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. 
 
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..c9d46428 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,13 +4,12 @@ open Lake DSL System
 package «sampcert» where
   testDriver := "test"
 
+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"
 
--- From doc-gen4
-meta if get_config? env = some "doc" then
-require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
-
 target ffi.o (pkg : NPackage __name__) : FilePath := do
   let oFile := pkg.buildDir / "ffi.o"
   let srcFile ← inputFile (pkg.dir / "ffi.cpp") false