Skip to content

Commit

Permalink
Add CI that builds and deploys the spec to Pages
Browse files Browse the repository at this point in the history
  • Loading branch information
survived committed Jan 15, 2024
1 parent bd11179 commit c556245
Show file tree
Hide file tree
Showing 2 changed files with 95 additions and 0 deletions.
83 changes: 83 additions & 0 deletions .github/workflows/docs.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,83 @@
name: Build CGGMP21 Spec & Docs

on:
pull_request:
branches: [ "*" ]
paths:
- 'cggmp21/**'
- 'spec/**'
- '.github/workflows/docs.yml'
push:
branches: [ "m" ]

jobs:
build_pdf:
runs-on: ubuntu-latest
permissions:
pull-requests: write
steps:
- uses: actions/checkout@v3
- name: Compile LaTeX document
uses: xu-cheng/latex-action@v3
with:
root_file: spec/main.tex
working_directory: spec
- name: Rename PDF
run: mv main.pdf specs.pdf
- name: Upload artifacts
uses: actions/upload-artifact@v4
with:
name: spec-pdf
path: spec.pdf
- name: Leave PR comment
continue-on-error: true
uses: marocchino/sticky-pull-request-comment@v2
with:
header: spec_is_built
message: The spec was successfully compiled. PDF is available in the artifacts.
build_docs:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- uses: dtolnay/rust-toolchain@nightly
- uses: Swatinem/rust-cache@v2
with:
cache-on-failure: "true"
- name: Build docs
run: make docs && cp docs/redirect.html target/doc/index.html
- name: Upload docs
uses: actions/upload-artifact@v3
with:
name: docs
path: target/doc
deploy_pages:
runs-on: ubuntu-latest
needs: [build_pdf, build_docs]
# if: github.ref == 'refs/heads/m'
environment:
name: github-pages
url: ${{ steps.deployment.outputs.page_url }}
permissions:
pages: write
id-token: write
steps:
- uses: actions/download-artifact@v3
with:
name: docs
path: website
- uses: actions/download-artifact@v3
with:
name: spec-pdf
path: website/cggmp21-spec.pdf
- name: Prepare Github Pages deployment
run: |
mkdir public
cp README.md public/index.md
cp cggmp21-specs.pdf public
- name: Upload artifact
uses: actions/upload-pages-artifact@v3
with:
path: 'website'
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v4
12 changes: 12 additions & 0 deletions docs/redirect.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
<!-- This file is meant to be an entry point of Github Pages -->

<head>
<meta http-equiv="Refresh" content="0; URL=cggmp21/index.html" />
<title>Redirection</title>
</head>

<body>
<p>
You are being redirected to another page. Click <a href="cggmp21/index.html">here</a> if it didn't work.
</p>
</body>

0 comments on commit c556245

Please sign in to comment.