Skip to content

Commit f5d03ed

Browse files
feat: use docgen-action for documentation generation (#128)
Uses leanprover-community/docgen-action to build & deploy docs. Closes #121 --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
1 parent 0e03035 commit f5d03ed

6 files changed

Lines changed: 33 additions & 160 deletions

File tree

.github/workflows/docs.yml

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
name: Build and Deploy Documentation
2+
3+
on:
4+
push:
5+
branches:
6+
- main # Build docs on merges to main
7+
workflow_dispatch:
8+
9+
permissions:
10+
contents: read
11+
id-token: write
12+
pages: write
13+
14+
jobs:
15+
build:
16+
runs-on: ubuntu-latest
17+
steps:
18+
- name: Checkout project
19+
uses: actions/checkout@v4
20+
with:
21+
fetch-depth: 0
22+
23+
- name: Build and lint the project
24+
id: build-lean
25+
uses: leanprover/lean-action@v1
26+
with:
27+
build-args: "--wfail"
28+
29+
- name: Build project documentation
30+
id: build-docgen
31+
uses: leanprover-community/docgen-action@main
32+
with:
33+
build-page: false

.github/workflows/lean_action_ci.yml

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,6 @@ jobs:
1010
runs-on: ubuntu-latest
1111
steps:
1212
- uses: actions/checkout@v4
13-
- if: github.event_name == 'pull_request' || (github.event_name == 'push' && github.ref == 'refs/heads/main')
14-
run: |
15-
set -e
16-
cmp -s lean-toolchain docs/lean-toolchain
1713
- uses: leanprover/lean-action@v1
1814
with:
1915
build-args: "--wfail"

docs/lake-manifest.json

Lines changed: 0 additions & 142 deletions
This file was deleted.

docs/lakefile.toml

Lines changed: 0 additions & 13 deletions
This file was deleted.

docs/lean-toolchain

Lines changed: 0 additions & 1 deletion
This file was deleted.
File renamed without changes.

0 commit comments

Comments
 (0)