Skip to content

Commit

Permalink
feat: try to get docs working again using mathlib style upload artifact
Browse files Browse the repository at this point in the history
Instead of pushing to a branch, upload docs as an artifact,
which does not have a 100MB push limit.
  • Loading branch information
bollu committed Oct 25, 2023
1 parent 88e31c2 commit 958524d
Show file tree
Hide file tree
Showing 2 changed files with 41 additions and 3 deletions.
12 changes: 9 additions & 3 deletions .github/workflows/doc.yml
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,14 @@ jobs:
- name: Generate docs 📜
run: |
./docgen.sh
- name: Deploy 🚀
uses: JamesIves/github-pages-deploy-action@v4
# stolen from mathlib: https://github.com/leanprover-community/mathlib4_docs/blob/1f4ea7657bc377b4298fd400e567471d3a248b2d/.github/workflows/docs.yaml#L79-L86
- name: Upload artifact 📁
uses: actions/upload-pages-artifact@v1
with:
folder: build/doc # The folder the action should deploy.
path: 'build/doc'

- name: Deploy to GitHub Pages 🚀
id: deployment
uses: actions/deploy-pages@v1

32 changes: 32 additions & 0 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,14 @@
"name": "partax",
"inputRev?": "master",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover/doc-gen4",
"subDir?": null,
"rev": "8bccb92b531248af1b6692d65486e8640c8bcd10",
"opts": {},
"name": "«doc-gen4»",
"inputRev?": "8bccb92b531248af1b6692d65486e8640c8bcd10",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
Expand Down Expand Up @@ -56,5 +64,29 @@
"opts": {},
"name": "proofwidgets",
"inputRev?": "v0.0.19",
"inherited": true}},
{"git":
{"url": "https://github.com/xubaiw/CMark.lean",
"subDir?": null,
"rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
"opts": {},
"name": "CMark",
"inputRev?": "main",
"inherited": true}},
{"git":
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
"subDir?": null,
"rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32",
"opts": {},
"name": "«lean4-unicode-basic»",
"inputRev?": "main",
"inherited": true}},
{"git":
{"url": "https://github.com/hargonix/LeanInk",
"subDir?": null,
"rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
"opts": {},
"name": "leanInk",
"inputRev?": "doc-gen",
"inherited": true}}],
"name": "SSA"}

0 comments on commit 958524d

Please sign in to comment.