linglib/.github/workflows/docs.yml at 5b15b21580408b5a464759a912522bc081025de9 · hawkrobe/linglib · 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
128
129
130
131
132
133
134
name: Build and Deploy Docs

on:
  push:
    branches: [main]
  workflow_dispatch:

env:
  ELAN_NO_OVERRIDE_NOTICE: 1

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

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

jobs:
  build:
    runs-on: ubuntu-latest
    timeout-minutes: 120
    steps:
      - name: Checkout
        uses: actions/checkout@v4
        with:
          submodules: true

      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: Install and activate toolchain
        run: |
          elan toolchain install $(cat lean-toolchain)
          elan override set $(cat lean-toolchain)
          lake --version

      - name: Cache .lake
        uses: actions/cache@v4
        with:
          path: .lake
          key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-docs-${{ hashFiles('Linglib/**/*.lean', 'Linglib.lean') }}
          restore-keys: |
            lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-docs-
            lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-

      - name: Get Mathlib cache
        run: lake exe cache get

      - name: Build project
        run: lake build

      - name: Build documentation (Linglib only, skip Mathlib)
        run: |
          # Use doc-gen4 CLI directly to avoid Lake facet processing ALL
          # transitive deps (Mathlib/Lean core), which OOMs the runner.
          lake build doc-gen4

          BUILD=.lake/build
          DOCGEN="lake exe doc-gen4"
          REPO_URL="https://github.com/${{ github.repository }}"
          COMMIT="${{ github.sha }}"
          SRC_URI="$REPO_URL/blob/$COMMIT"
          DB=api-docs.db

          # Remove stale DB — schema changes across doc-gen4 versions
          # cause "no such table" errors if an old DB is reused.
          # Delete both possible locations (build dir and repo root).
          rm -f "$BUILD/$DB" "$DB"

          # Bibliography prepass
          if [ -f docs/references.bib ]; then
            $DOCGEN bibPrepass --build "$BUILD" docs/references.bib
          elif [ -f docs/references.json ]; then
            $DOCGEN bibPrepass --build "$BUILD" --json docs/references.json
          else
            $DOCGEN bibPrepass --build "$BUILD" --none
          fi

          # Document root module (may fail if Linglib.olean missing — non-fatal)
          $DOCGEN single --build "$BUILD" Linglib "$DB" "$SRC_URI/Linglib.lean" || true

          # Document all Linglib submodules
          find Linglib -name '*.lean' | sort | while read -r f; do
            mod=$(echo "$f" | sed 's|/|.|g; s|\.lean$||')
            echo "  doc: $mod"
            $DOCGEN single --build "$BUILD" "$mod" "$DB" "$SRC_URI/$f" || true
          done

          # Generate HTML + search index from database
          # NOTE: fromDb treats the db arg as a literal path (not relative
          # to --build), unlike single/genCore which prepend --build.
          $DOCGEN fromDb --build "$BUILD" "$BUILD/$DB"

      - name: Install Hugo
        uses: peaceiris/actions-hugo@v3
        with:
          hugo-version: 'latest'
          extended: true

      - name: Build blog
        working-directory: blog
        run: hugo --minify

      - name: Compose site
        run: |
          mkdir -p .lake/build/doc-site
          # Hugo output → site root
          cp -r blog/public/* .lake/build/doc-site/
          # doc-gen4 output → /docs/ subdirectory
          mkdir -p .lake/build/doc-site/docs
          cp -r .lake/build/doc/* .lake/build/doc-site/docs/

      - name: Setup Pages
        uses: actions/configure-pages@v4

      - name: Upload artifact
        uses: actions/upload-pages-artifact@v3
        with:
          path: '.lake/build/doc-site'

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