feat: generate docs from subdirectory #1028

fgdorais · 2024-11-07T22:08:00Z

This uses the idea proposed by Sebastian Ullrich on Zulip in order to streamline generating doc-gen4 documentations for batteries.

BatteriesDocs.lean

Co-authored-by: Kim Morrison <kim@tqft.net>

leanprover-community-bot · 2024-11-07T22:40:19Z

Mathlib CI status (docs):

🟡 Mathlib branch batteries-pr-testing-1028 build against this PR was cancelled. (2024-11-07 22:40:18) View Log
🟡 Mathlib branch batteries-pr-testing-1028 build against this PR was cancelled. (2024-11-07 23:36:28) View Log
🟡 Mathlib branch batteries-pr-testing-1028 build against this PR was cancelled. (2024-11-07 23:53:19) View Log
✅ Mathlib branch batteries-pr-testing-1028 has successfully built against this PR. (2024-11-08 00:27:50) View Log
🟡 Mathlib branch batteries-pr-testing-1028 build against this PR was cancelled. (2024-11-08 00:52:18) View Log
✅ Mathlib branch batteries-pr-testing-1028 has successfully built against this PR. (2024-11-08 01:28:51) View Log
🟡 Mathlib branch batteries-pr-testing-1028 build against this PR was cancelled. (2024-11-09 17:54:55) View Log
🟡 Mathlib branch batteries-pr-testing-1028 build against this PR was cancelled. (2024-11-09 18:01:24) View Log
✅ Mathlib branch batteries-pr-testing-1028 has successfully built against this PR. (2024-11-09 18:36:51) View Log
✅ Mathlib branch batteries-pr-testing-1028 has successfully built against this PR. (2024-11-09 23:46:05) View Log
✅ Mathlib branch batteries-pr-testing-1028 has successfully built against this PR. (2024-11-10 02:49:58) View Log
🟡 Mathlib branch batteries-pr-testing-1028 build against this PR was cancelled. (2024-11-10 03:53:36) View Log
✅ Mathlib branch batteries-pr-testing-1028 has successfully built against this PR. (2024-11-10 04:29:46) View Log
✅ Mathlib branch batteries-pr-testing-1028 has successfully built against this PR. (2024-11-11 00:26:12) View Log
✅ Mathlib branch batteries-pr-testing-1028 has successfully built against this PR. (2024-11-11 05:40:56) View Log
✅ Mathlib branch batteries-pr-testing-1028 has successfully built against this PR. (2024-11-11 06:39:41) View Log
🟡 Mathlib branch batteries-pr-testing-1028 build against this PR was cancelled. (2024-11-11 09:33:22) View Log
🟡 Mathlib branch batteries-pr-testing-1028 build this PR didn't complete normally. (2024-11-11 09:33:27) View Log
✅ Mathlib branch batteries-pr-testing-1028 has successfully built against this PR. (2024-11-11 10:16:53) View Log
✅ Mathlib branch batteries-pr-testing-1028 has successfully built against this PR. (2024-11-12 02:10:33) View Log
✅ Mathlib branch batteries-pr-testing-1028 has successfully built against this PR. (2024-11-12 09:59:10) View Log

docs/lakefile.toml

BatteriesDocs/lean-toolchain

.github/workflows/docs-deploy.yml

fgdorais · 2024-11-12T09:19:31Z

The documentation setup is now fully in line with the new recommendations at doc-gen4. The docs directory name and the buildDir = "." addition is to facilitate deployment to github pages.

feat: generate docs from subdirectory

a342991

fgdorais added the WIP work in progress label Nov 7, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 7, 2024

Update Batteries branch for testing leanprover-community/batteries#1028

49d63bb

kim-em reviewed Nov 7, 2024

View reviewed changes

BatteriesDocs.lean Outdated Show resolved Hide resolved

kim-em mentioned this pull request Nov 7, 2024

Lake's defaultTargets should allow specifying a facet. leanprover/lean4#6003

Open

fix: typo

d7baef8

Co-authored-by: Kim Morrison <kim@tqft.net>

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 7, 2024

Trigger CI for leanprover-community/batteries#1028

b36b4f8

feat: add release workflow

d605f88

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 7, 2024

Trigger CI for leanprover-community/batteries#1028

57e7730

fix: use docs directory

10fb06d

fgdorais force-pushed the batteries-docs branch from 549b132 to 10fb06d Compare November 7, 2024 23:32

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 7, 2024

Trigger CI for leanprover-community/batteries#1028

fcdb2f8

fix: use existing lake manifest

0a96b35

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 7, 2024

Trigger CI for leanprover-community/batteries#1028

ab8b896

leanprover-community-bot added the builds-mathlib label Nov 8, 2024

fix: reduce noise from lake build

3bb5229

fgdorais marked this pull request as ready for review November 8, 2024 00:45

fgdorais added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed WIP work in progress labels Nov 8, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 8, 2024

Trigger CI for leanprover-community/batteries#1028

20d2d04

chore: update README

29a66f8

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 8, 2024

Trigger CI for leanprover-community/batteries#1028

3509f4b

chore: add deployment step

87da4b0

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 9, 2024

Trigger CI for leanprover-community/batteries#1028

ab3ce1c

chore: add docs deployment step

7bac6e0

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 9, 2024

Trigger CI for leanprover-community/batteries#1028

775c436

chore: update docs

c85e8fc

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 9, 2024

Trigger CI for leanprover-community/batteries#1028

97ed283

refactor: docs workflows

bfdc7e4

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 10, 2024

Trigger CI for leanprover-community/batteries#1028

c212136

chore: default github pages root to readme

df2bcca

fgdorais force-pushed the batteries-docs branch from f5f4649 to df2bcca Compare November 10, 2024 03:51

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 10, 2024

Trigger CI for leanprover-community/batteries#1028

6b2eec5

digama0 reviewed Nov 10, 2024

View reviewed changes

docs/lakefile.toml Outdated Show resolved Hide resolved

refactor: reorganize directories

6e2cd41

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 10, 2024

Trigger CI for leanprover-community/batteries#1028

851aa86

digama0 reviewed Nov 11, 2024

View reviewed changes

BatteriesDocs/lean-toolchain Outdated Show resolved Hide resolved

fix: remove unnecessary lean-toolchain symlink

c13ced7

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 11, 2024

Trigger CI for leanprover-community/batteries#1028

2780416

refactor: reorganize docs template

1a3fe2e

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 11, 2024

Trigger CI for leanprover-community/batteries#1028

5cabee9

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 11, 2024

Trigger CI for leanprover-community/batteries#1028

fb382f1

fgdorais force-pushed the batteries-docs branch from 98bd5e2 to 01a1bc9 Compare November 11, 2024 09:30

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 11, 2024

Trigger CI for leanprover-community/batteries#1028

a944283

refactor: further simplify setup

9556fbc

fgdorais force-pushed the batteries-docs branch from 01a1bc9 to 9556fbc Compare November 11, 2024 09:33

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 11, 2024

Trigger CI for leanprover-community/batteries#1028

494c6c7

chore: improve once more

a6f7435

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 12, 2024

Trigger CI for leanprover-community/batteries#1028

f813a4a

fgdorais commented Nov 12, 2024

View reviewed changes

.github/workflows/docs-deploy.yml Outdated Show resolved Hide resolved

fix: missing detail

c3624ff

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 12, 2024

Trigger CI for leanprover-community/batteries#1028

d7a23d6

chore: use reservoir style require in docs

21fa97f

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 12, 2024

Trigger CI for leanprover-community/batteries#1028

c51a3f9

fgdorais added this pull request to the merge queue Nov 12, 2024

Merged via the queue into main with commit e6047ba Nov 12, 2024
3 checks passed

github-actions bot removed the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Nov 12, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: generate docs from subdirectory #1028

feat: generate docs from subdirectory #1028

fgdorais commented Nov 7, 2024

leanprover-community-bot commented Nov 7, 2024 •

edited

Loading

fgdorais commented Nov 12, 2024

feat: generate docs from subdirectory #1028

feat: generate docs from subdirectory #1028

Conversation

fgdorais commented Nov 7, 2024

leanprover-community-bot commented Nov 7, 2024 • edited Loading

fgdorais commented Nov 12, 2024

leanprover-community-bot commented Nov 7, 2024 •

edited

Loading