wip: inductive ctors #868
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| on: | |
| push: | |
| pull_request: | |
| name: Continuous Integration | |
| jobs: | |
| build: | |
| name: test | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: install elan | |
| run: | | |
| set -o pipefail | |
| curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz | |
| ./elan-init -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - uses: actions/checkout@v3 | |
| - name: List all files | |
| run: | | |
| find . -name "*.lean" -type f | |
| - name: lean version | |
| run: | | |
| lean --version | |
| - name: Compute short SHA | |
| id: shortSHA | |
| run: echo "short_sha=$(git rev-parse --short HEAD)" >> $GITHUB_OUTPUT | |
| - name: Cache .lake | |
| uses: actions/cache@v4 | |
| with: | |
| path: .lake | |
| # The SHA is in the key to get the most recent cache possible, rather than just saving a single one for each Lean/deps version and not touching it. | |
| key: ${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lean-toolchain') }}-${{ steps.shortSHA.outputs.short_sha }} | |
| # Try to restore cache for same OS/Lean/deps, but don't get less specific, because Lake isn't always happy to get build product version mismatches | |
| restore-keys: | | |
| ${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lean-toolchain') }}- | |
| - name: Build the project | |
| run: | | |
| lake build | |
| - name: Generate the example website | |
| run: | | |
| lake exe demosite --output _out/examples/demosite | |
| - name: Generate the example genre's document | |
| run: | | |
| lake exe simplepage | |
| - name: Check internal links on the example website | |
| uses: lycheeverse/[email protected] | |
| with: | |
| format: markdown | |
| jobSummary: true | |
| args: --base './_out/examples/demosite' --no-progress --offline './_out/examples/demosite/**/*.html' | |
| - name: Check for consistent Subverso versions in all manifests | |
| run: | | |
| echo "Subverso versions:" | |
| find . -name lake-manifest.json -print0 | xargs -0 jq '.packages[] | select(.name == "subverso") | {"file": input_filename, "subverso": .rev}' | |
| find . -name lake-manifest.json -print0 | xargs -0 jq -e -s 'map(.packages[] | select(.name == "subverso").rev) | .[0] as $x | all(.[]; . == $x)' | |
| - name: Install PDF Dependencies | |
| uses: teatimeguest/setup-texlive-action@v3 | |
| with: | |
| packages: | | |
| scheme-minimal | |
| latex-bin | |
| xpatch | |
| xparse | |
| array | |
| booktabs | |
| footmisc | |
| environ | |
| hyperref | |
| titlesec | |
| tocloft | |
| enumitem | |
| fmtcount | |
| glossaries | |
| datatool | |
| caption | |
| babel | |
| fontspec | |
| textcase | |
| memoir | |
| sourcecodepro | |
| sourcesanspro | |
| sourceserifpro | |
| fvextra | |
| - name: Check `tlmgr` version | |
| run: tlmgr --version | |
| - name: Generate the manual | |
| run: | | |
| ./generate.sh | |
| cp _out/tex/main.pdf ./manual.pdf | |
| cp -r _out/html-single html-single-page | |
| zip -r html-single-page.zip html-single-page | |
| - name: Upload docs to artifact storage | |
| if: github.ref != 'refs/heads/main' | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: "Verso manual (PDF and HTML)" | |
| path: | | |
| manual.pdf | |
| html-single-page.zip | |
| - uses: "marvinpinto/action-automatic-releases@latest" | |
| if: github.ref == 'refs/heads/main' | |
| with: | |
| repo_token: "${{ secrets.GITHUB_TOKEN }}" | |
| automatic_release_tag: "latest" | |
| title: "Verso manual (PDF and HTML)" | |
| files: | | |
| manual.pdf | |
| html-single-page.zip | |