refactor: reorganize docs template

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

Hide file tree

Showing 4 changed files with 20 additions and 27 deletions.
diff --git a/BatteriesDocs.lean b/BatteriesDocs.lean
diff --git a/docs/docs.lean b/docs/docs.lean
@@ -0,0 +1,15 @@
+/- Import project roots here -/
+import Batteries
+
+/-! # Documentation
+
+To generate documentation for this project:
+
+```sh
+cd docs
+lake build
+```
+
+The [`doc-gen4`](https://github.com/leanprover/doc-gen4) documentation will be found in the
+`docs/doc` and `docs/doc-data` subdirectories.
+-/
diff --git a/BatteriesDocs/lake-manifest.json → docs/lake-manifest.json b/BatteriesDocs/lake-manifest.json → docs/lake-manifest.json
@@ -58,5 +58,5 @@
    "inherited": false,
    "dir": "./..",
    "configFile": "lakefile.toml"}],
- "name": "«batteries-docs»",
+ "name": "docs",
  "lakeDir": ".lake"}
diff --git a/BatteriesDocs/lakefile.toml → docs/lakefile.toml b/BatteriesDocs/lakefile.toml → docs/lakefile.toml
@@ -1,7 +1,7 @@
-name = "batteries-docs"
+name = "docs"
 reservoir = false
-buildDir = "../docs"
-defaultTargets = ["BatteriesDocs"]
+buildDir = "."
+defaultTargets = ["docs"]
 
 [[require]]
 name = "doc-gen4"
@@ -13,6 +13,5 @@ name = "batteries"
 path = ".."
 
 [[lean_lib]]
-name = "BatteriesDocs"
-srcDir = ".."
+name = "docs"
 defaultFacets = ["docs"]