Continuous Integration #3122
Workflow file for this run
This file contains hidden or 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: | |
| branches: | |
| - master | |
| - main | |
| - nightly-testing | |
| pull_request: | |
| merge_group: | |
| name: Continuous Integration | |
| jobs: | |
| build: | |
| name: Build and test | |
| runs-on: nscloud-ubuntu-22.04-amd64-8x16 | |
| env: | |
| # Used for browser tests. Placing them here allows caching to work right. | |
| PLAYWRIGHT_BROWSERS_PATH: ${{ github.workspace }}/.playwright-browsers | |
| 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@v7 | |
| - 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@v6 | |
| 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') }}- | |
| # This was failing CI from clang crashing, so do it first for fast turnaround | |
| - name: Build the website examples subproject | |
| run: | | |
| pushd test-projects/website-examples | |
| lake build | |
| lake build :examples | |
| popd | |
| - name: Build the project | |
| run: | | |
| lake build | |
| - name: Install PDF Dependencies | |
| uses: ./.github/actions/install-texlive | |
| # Inkscape is needed by the LaTeX `svg` package, which converts | |
| # SVG files emitted by `diagram` code blocks to PDF at build time. | |
| - name: Install Inkscape | |
| run: sudo apt-get update && sudo apt-get install -y --no-install-recommends inkscape | |
| # Install uv and Playwright before tests, since lake test | |
| # runs literate browser tests that need them | |
| - name: Install uv | |
| uses: astral-sh/setup-uv@v7 | |
| with: | |
| enable-cache: true | |
| cache-dependency-glob: "browser-tests/pyproject.toml" | |
| - name: Cache Playwright browsers | |
| uses: actions/cache@v6 | |
| with: | |
| path: .playwright-browsers | |
| key: playwright-${{ runner.os }}-${{ hashFiles('browser-tests/uv.lock') }} | |
| - name: Install Playwright browsers | |
| run: | | |
| uv run --project browser-tests --extra test playwright install chromium firefox --with-deps | |
| # The LaTeX `svg` package shells out to `inkscape --version` during | |
| # the `--check-tex` build. Fail here with a clear message if Inkscape | |
| # is missing or its version can't be read, rather than deep inside a | |
| # lualatex run. | |
| - name: Check Inkscape is available | |
| run: | | |
| inkscape --version | |
| - name: Run tests | |
| run: | | |
| lake test -- --verbose --check-tex | |
| - name: Test the dev server | |
| run: | | |
| ./src/tests/run_serve_test.sh | |
| - name: Generate the test website | |
| run: | | |
| lake exe demosite --output _out/test-projects/demosite | |
| - name: Generate the test genre's document | |
| run: | | |
| lake exe simplepage | |
| - name: Generate some source HTML | |
| run: | | |
| lake build Verso.Hover:literate | |
| lake exe verso-html .lake/build/literate htmlout | |
| - name: Install linkchecker | |
| run: pip install linkchecker | |
| - name: Check internal links on the test website | |
| run: | | |
| linkchecker --config=.linkchecker/linkcheckerrc --no-status ./_out/test-projects/demosite/ | |
| - name: Generate the test tutorial site | |
| run: | | |
| lake exe tutorial-example | |
| - name: Check internal links on the test tutorial site | |
| run: | | |
| linkchecker --config=.linkchecker/linkcheckerrc --no-status ./_out/tut/ | |
| - name: Generate the manual | |
| run: | | |
| ./generate.sh | |
| cp _out/tex/main.pdf ./manual.pdf | |
| cp -r _out/html-multi html-multi | |
| cp README-html.md html-multi/README.md | |
| zip -r html-manual.zip html-multi | |
| - uses: actions/setup-node@v7 | |
| with: | |
| node-version: "lts/*" | |
| cache: npm | |
| - run: npm ci | |
| - name: Type check the search bar code | |
| run: | | |
| pushd _out/html-multi/-verso-search | |
| npx tsc --noEmit -p jsconfig.json | |
| popd | |
| - name: Type check the xref redirect JS code | |
| run: | | |
| pushd static-web | |
| npx tsc --noEmit -p jsconfig.json | |
| popd | |
| - name: Check the ToC width storage key stays in sync | |
| run: | | |
| # toc-resize.js and toc-resize-preload.js must agree on the localStorage | |
| # key, since the preload primes the value the main script later reads. | |
| main_key=$(grep -oE 'STORAGE_KEY = "[^"]+"' static-web/toc-resize.js | grep -oE '"[^"]+"') | |
| preload_key=$(grep -oE 'getItem\("[^"]+"\)' static-web/toc-resize-preload.js | grep -oE '"[^"]+"') | |
| echo "toc-resize.js storage key: ${main_key:-<none>}" | |
| echo "toc-resize-preload.js storage key: ${preload_key:-<none>}" | |
| if [ -z "$main_key" ] || [ -z "$preload_key" ]; then | |
| echo "::error::Could not find the ToC width storage key in one of the scripts" >&2 | |
| exit 1 | |
| fi | |
| if [ "$main_key" != "$preload_key" ]; then | |
| echo "::error::ToC width localStorage key differs between toc-resize.js and toc-resize-preload.js" >&2 | |
| exit 1 | |
| fi | |
| - name: Generate the demo site and make sure page_link works | |
| run: | | |
| lake exe demosite --output _out/demosite | |
| # Fail if the generated about page doesn't have the expected base tag and blog link | |
| grep -qF '<a href="blog/">blog</a> genre' _out/demosite/about/index.html | |
| grep -qF '<base href=".././">' _out/demosite/about/index.html | |
| # uv and Playwright are installed before `lake test` above. | |
| - name: Cache literate-config test project | |
| uses: actions/cache@v6 | |
| with: | |
| path: test-projects/literate-config/.lake | |
| key: | |
| literate-config-${{ runner.os }}-${{ | |
| hashFiles('test-projects/literate-config/lean-toolchain') }}-${{ | |
| hashFiles('test-projects/literate-config/lake-manifest.json') }}-${{ | |
| steps.shortSHA.outputs.short_sha }} | |
| restore-keys: | | |
| literate-config-${{ runner.os }}-${{ hashFiles('test-projects/literate-config/lean-toolchain') }}-${{ hashFiles('test-projects/literate-config/lake-manifest.json') }}- | |
| - name: Cache literate-multi-root test project | |
| uses: actions/cache@v6 | |
| with: | |
| path: test-projects/literate-multi-root/.lake | |
| key: | |
| literate-multi-root-${{ runner.os }}-${{ | |
| hashFiles('test-projects/literate-multi-root/lean-toolchain') }}-${{ | |
| hashFiles('test-projects/literate-multi-root/lake-manifest.json') }}-${{ | |
| steps.shortSHA.outputs.short_sha }} | |
| restore-keys: | | |
| literate-multi-root-${{ runner.os }}-${{ hashFiles('test-projects/literate-multi-root/lean-toolchain') }}-${{ hashFiles('test-projects/literate-multi-root/lake-manifest.json') }}- | |
| - name: Run literate browser tests | |
| run: src/tests/run_literate_browser_tests.sh | |
| - name: Run browser tests | |
| run: | | |
| uv run --project browser-tests --extra test pytest \ | |
| browser-tests/test_search.py \ | |
| browser-tests/test_search_priority.py \ | |
| browser-tests/test_search_page.py \ | |
| browser-tests/test_toc_resize.py \ | |
| browser-tests/test_redirect.py \ | |
| browser-tests/test_katex.py -v | |
| - name: Build the VersoHtml site for browser tests | |
| run: | | |
| # The verso-html genre renders literate JSON into a standalone HTML site. | |
| # We reuse the literate-config test project (already cached) as input, then | |
| # run verso-html against its literate-JSON output. | |
| pushd test-projects/literate-config | |
| lake build +LitConfig:literate | |
| popd | |
| lake exe verso-html test-projects/literate-config/.lake/build/literate _out/verso-html | |
| - name: Run VersoHtml browser tests | |
| run: | | |
| uv run --project browser-tests --extra test pytest \ | |
| browser-tests/verso-html -v \ | |
| --site-dir "$(pwd)/_out/verso-html" | |
| - name: Upload docs to artifact storage | |
| if: github.ref != 'refs/heads/main' | |
| uses: actions/upload-artifact@v7 | |
| with: | |
| name: "Verso manual (PDF and HTML)" | |
| path: | | |
| manual.pdf | |
| html-manual.zip | |
| - uses: "marvinpinto/action-automatic-releases@v1.2.1" | |
| 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-manual.zip | |
| # deploy-info computes metadata that's shown in the Netlify interface | |
| # about the deployment (for non-PR deploys) | |
| - id: deploy-info | |
| name: Compute Deployment Metadata | |
| if: github.event_name != 'pull_request' | |
| run: | | |
| set -e | |
| echo "message=$(git log -1 --pretty=format:"%s")" >> "$GITHUB_OUTPUT" | |
| - name: Upload HTML manual for PR deployment | |
| if: github.event_name == 'pull_request' | |
| uses: actions/upload-artifact@v7 | |
| with: | |
| name: html-manual-for-deploy | |
| path: _out/html-multi | |
| retention-days: 1 | |
| - name: Deploy Verso manual | |
| id: deploy-lang | |
| uses: nwtgck/actions-netlify@v4.0 | |
| if: github.event_name == 'push' && github.ref_name == 'main' | |
| with: | |
| publish-dir: _out/html-multi | |
| production-branch: main | |
| github-token: ${{ secrets.GITHUB_TOKEN }} | |
| alias: ref-${{ github.ref_name }} | |
| deploy-message: | |
| "ref/${{ github.ref_name }}: ${{ steps.deploy-info.outputs.message }}" | |
| enable-commit-comment: false | |
| github-deployment-environment: verso-main | |
| fails-without-credentials: true | |
| env: | |
| NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }} | |
| NETLIFY_SITE_ID: "8a89abd8-095b-4496-a9c1-381d2d5629ec" # TODO: if a tag, push to a different site for hosting under lean-lang.org |