From 1a3fe2e8e46f0ceb8ea084a5596a1d5f6fb90883 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Mon, 11 Nov 2024 00:55:10 -0500
Subject: [PATCH] refactor: reorganize docs template

---
 BatteriesDocs.lean                         | 21 ---------------------
 docs/docs.lean                             | 15 +++++++++++++++
 {BatteriesDocs => docs}/lake-manifest.json |  2 +-
 {BatteriesDocs => docs}/lakefile.toml      |  9 ++++-----
 4 files changed, 20 insertions(+), 27 deletions(-)
 delete mode 100644 BatteriesDocs.lean
 create mode 100644 docs/docs.lean
 rename {BatteriesDocs => docs}/lake-manifest.json (98%)
 rename {BatteriesDocs => docs}/lakefile.toml (62%)

diff --git a/BatteriesDocs.lean b/BatteriesDocs.lean
deleted file mode 100644
index 19a5943055..0000000000
--- a/BatteriesDocs.lean
+++ /dev/null
@@ -1,21 +0,0 @@
-/-
-Copyright (c) 2024 François G. Dorais. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: François G. Dorais
--/
-
-import Batteries
-
-/-! # Batteries Documentation
-
-To generate documentation for Batteries:
-
-```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/docs/docs.lean b/docs/docs.lean
new file mode 100644
index 0000000000..5719d88a8d
--- /dev/null
+++ 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 b/docs/lake-manifest.json
similarity index 98%
rename from BatteriesDocs/lake-manifest.json
rename to docs/lake-manifest.json
index acc6dbfcf5..25f3db728e 100644
--- a/BatteriesDocs/lake-manifest.json
+++ b/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 b/docs/lakefile.toml
similarity index 62%
rename from BatteriesDocs/lakefile.toml
rename to docs/lakefile.toml
index bbcc51746a..c4899e71ea 100644
--- a/BatteriesDocs/lakefile.toml
+++ b/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"]