Skip to content

Commit

Permalink
chore: setup github pages docs deploy
Browse files Browse the repository at this point in the history
  • Loading branch information
thelissimus committed Nov 10, 2024
1 parent ac584f3 commit dc023b8
Showing 1 changed file with 52 additions and 0 deletions.
52 changes: 52 additions & 0 deletions .github/workflows/ghpages.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
name: Documentation

on:
push:
branches: ["master"]
workflow_dispatch:

permissions:
contents: read
pages: write
id-token: write

concurrency:
group: "pages"
cancel-in-progress: true

jobs:
build:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4
- id: lean-action
name: Build and test
uses: leanprover/lean-action@v1
with:
lint-module: TTFPI
use-github-cache: false
- name: Build Doc
run: |
lake -R -Kenv=dev update
lake -R -Kenv=dev build TTFPI:docs
- name: Setup Pages
uses: actions/configure-pages@v4
- name: Upload artifact
uses: actions/upload-pages-artifact@v3
with:
path: './.lake/build/doc'

deploy:
needs: build
permissions:
pages: write
id-token: write
environment:
name: github-pages
url: ${{ steps.deployment.outputs.page_url }}
runs-on: ubuntu-latest
steps:
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v4

0 comments on commit dc023b8

Please sign in to comment.