complexitylib/.github/workflows/docs.yml at dev · SamuelSchlesinger/complexitylib · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
name: API Documentation and Blueprint

# Building doc-gen4 documentation also generates pages for Mathlib, which is
# slow. It runs on every push to the default branch (dev) so the published API
# docs track the code, plus weekly and on demand. The `pages` concurrency
# group below cancels a superseded in-progress run, so rapid merges don't pile
# up. The blueprint (blueprint/) is built alongside and published under
# /blueprint.
on:
  push:
    branches: [dev]
  workflow_dispatch:
  schedule:
    - cron: "0 6 * * 1"

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

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

jobs:
  build-docs:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5
      - name: Install elan
        run: |
          curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y \
            --default-toolchain "$(cat lean-toolchain)"
          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
      - uses: actions/setup-python@v5
        with:
          python-version: "3.12"
      # plasTeX resolves `\input{chapters/...}` through TeX's `kpsewhich`;
      # without it every chapter is silently dropped, so install TeX's
      # binaries. The blueprint is built before the slow API docs so that a
      # broken blueprint fails the run within minutes.
      - name: Install blueprint toolchain
        run: |
          sudo apt-get update
          sudo apt-get install -y graphviz libgraphviz-dev texlive-base
          pip install leanblueprint
      - name: Build blueprint
        run: |
          set -o pipefail
          leanblueprint web 2>&1 | tee blueprint-build.log
          if grep -q "File not found" blueprint-build.log; then
            echo "::error::the blueprint build could not find some of its inputs"
            exit 1
          fi
          test -f blueprint/web/chap-intro.html
          test -f blueprint/web/dep_graph_document.html
      # Match Lean CI's exact dependency snapshot and incremental project
      # build. Docs can only see successful dev snapshots: PR project caches
      # have an isolated scope. Lake still validates restored project sources.
      - name: Restore Lean dependencies
        id: lean-deps
        uses: actions/cache/restore@caa296126883cff596d87d8935842f9db880ef25 # v5
        with:
          path: .lake/packages
          key: lean-deps-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json') }}
      - name: Restore project build
        uses: actions/cache/restore@caa296126883cff596d87d8935842f9db880ef25 # v5
        with:
          path: .lake/build
          key: lean-build-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json') }}-${{ github.sha }}
          restore-keys: lean-build-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json') }}-
      - name: Fetch Mathlib build cache
        run: lake exe cache get
      # Lean CI caches compiled modules, but not doc-gen4's expensive analysis.
      # This separate cache contains only dependency database rows and analysis
      # markers. Project declarations, source links, HTML, and search indexes
      # are always generated from the current checkout.
      - name: Fingerprint the public graph's dependency imports
        id: docs-imports
        run: |
          key=$(python3 scripts/cache_docs_dependencies.py --imports-key)
          echo "key=$key" >> "$GITHUB_OUTPUT"
      - name: Restore dependency documentation analysis
        id: docs-cache
        uses: actions/cache/restore@caa296126883cff596d87d8935842f9db880ef25 # v5
        with:
          path: docbuild/.lake/dependency-docs-cache
          key: docs-analysis-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('./lean-toolchain', './lakefile.toml', './lake-manifest.json', './docbuild/lean-toolchain', './docbuild/lakefile.toml', './docbuild/lake-manifest.json', './scripts/cache_docs_dependencies.py', './scripts/lint_style.py') }}-${{ steps.docs-imports.outputs.key }}
      - name: Seed the fresh documentation build
        run: |
          if test -d docbuild/.lake/dependency-docs-cache; then
            mkdir -p docbuild/.lake/build
            cp -a docbuild/.lake/dependency-docs-cache/. docbuild/.lake/build/
          fi
      - name: Build documentation
        working-directory: docbuild
        run: lake build Complexitylib:docs
      # Write only successful, trusted default-branch builds. Never cache HTML
      # or Complexitylib analysis, including deleted/renamed modules.
      - name: Stage dependency documentation analysis
        if: github.ref == 'refs/heads/dev' && steps.docs-cache.outputs.cache-hit != 'true'
        run: python3 scripts/cache_docs_dependencies.py
      - name: Save dependency documentation analysis
        if: github.ref == 'refs/heads/dev' && steps.docs-cache.outputs.cache-hit != 'true'
        uses: actions/cache/save@caa296126883cff596d87d8935842f9db880ef25 # v5
        with:
          path: docbuild/.lake/dependency-docs-cache
          key: ${{ steps.docs-cache.outputs.cache-primary-key }}
      - name: Publish the blueprint under /blueprint
        run: cp -r blueprint/web docbuild/.lake/build/doc/blueprint
      - name: Upload documentation artifact
        uses: actions/upload-pages-artifact@v3
        with:
          path: docbuild/.lake/build/doc

  deploy-docs:
    # Requires GitHub Pages to be enabled for the repository with
    # "GitHub Actions" as the source.
    needs: build-docs
    runs-on: ubuntu-latest
    environment:
      name: github-pages
      url: ${{ steps.deployment.outputs.page_url }}
    steps:
      - name: Deploy to GitHub Pages
        id: deployment
        uses: actions/deploy-pages@v4