From 9556fbcc0f61c04f2cb63fd9d8ba50081896bff5 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 11 Nov 2024 04:26:34 -0500 Subject: [PATCH] refactor: further simplify setup --- .github/workflows/docs-deploy.yml | 2 +- .github/workflows/docs-release.yml | 2 +- README.md | 6 +++--- docs/.gitignore | 1 + docs/docs.lean | 15 --------------- docs/lakefile.toml | 5 ----- 6 files changed, 6 insertions(+), 25 deletions(-) create mode 100644 docs/.gitignore delete mode 100644 docs/docs.lean diff --git a/.github/workflows/docs-deploy.yml b/.github/workflows/docs-deploy.yml index 0d5e833b6b..92ab030823 100644 --- 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 index 8585541153..2926a31340 100644 --- 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 index 4c63f289c1..ab9ec2d312 100644 --- 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 new file mode 100644 index 0000000000..01f8cdb637 --- /dev/null +++ b/docs/.gitignore @@ -0,0 +1 @@ +.lake/ diff --git a/docs/docs.lean b/docs/docs.lean deleted file mode 100644 index 5719d88a8d..0000000000 --- a/docs/docs.lean +++ /dev/null @@ -1,15 +0,0 @@ -/- 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/docs/lakefile.toml b/docs/lakefile.toml index c4899e71ea..9653eb60f5 100644 --- 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"]