refactor: further simplify setup

leanprover-community · Nov 11, 2024 · 9556fbc · 9556fbc
1 parent 1a3fe2e
commit 9556fbc
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 25 deletions.
diff --git a/.github/workflows/docs-deploy.yml b/.github/workflows/docs-deploy.yml
@@ -26,7 +26,7 @@ jobs:
 
       - name: Build Docs
         working-directory: docs
-        run: lake build -q
+        run: lake build -q Batteries:docs
 
       - name: Deploy Docs
         run: |

diff --git a/.github/workflows/docs-release.yml b/.github/workflows/docs-release.yml
@@ -27,7 +27,7 @@ jobs:
 
       - name: Build Docs
         working-directory: docs
-        run: lake build -q
+        run: lake build -q Batteries:docs
 
       - name: Compress Docs
         working-directory: docs

diff --git a/README.md b/README.md
@@ -31,15 +31,15 @@ Additionally, please make sure that you're using the version of Lean that the cu
 
 # Documentation
 
-You can generate `batteries`' documentation with
+You can generate `batteries` documentation with
 
 ```sh
 cd docs
-lake build
+lake build Batteries:docs
 ```
 
 The top-level HTML file will be located at `docs/doc/index.html`, though to actually expose the
-documentation as a server you need to change to the `docs/doc` and then run a HTTP server (e.g. `python3 -m http.server`).
+documentation you need to run a HTTP server (e.g. `python3 -m http.server`) in the `docs/doc` directory.
 
 Note that documentation for the latest nightly of `batteries` is also available as part of [the Mathlib 4
 documentation][mathlib4 docs].

diff --git a/docs/.gitignore b/docs/.gitignore
@@ -0,0 +1 @@
+.lake/
diff --git a/docs/docs.lean b/docs/docs.lean
diff --git a/docs/lakefile.toml b/docs/lakefile.toml
@@ -1,7 +1,6 @@
 name = "docs"
 reservoir = false
 buildDir = "."
-defaultTargets = ["docs"]
 
 [[require]]
 name = "doc-gen4"
@@ -11,7 +10,3 @@ rev = "main"
 [[require]]
 name = "batteries"
 path = ".."
-
-[[lean_lib]]
-name = "docs"
-defaultFacets = ["docs"]