Add Mac OS for lakefile.lean #16
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
| name: Compile blueprint | |
| on: | |
| push: | |
| branches: ["main"] | |
| pull_request: | |
| branches: ["main"] | |
| workflow_dispatch: | |
| concurrency: | |
| group: ${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: read | |
| env: | |
| FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true | |
| jobs: | |
| build_project: | |
| runs-on: ubuntu-latest | |
| name: Build project | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 1 | |
| - name: Free runner disk space | |
| run: | | |
| df -h | |
| sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /opt/hostedtoolcache/CodeQL || true | |
| sudo apt-get clean | |
| rm -rf ~/.cache/mathlib | |
| df -h | |
| - name: Install elan | |
| run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y | |
| - name: Get Mathlib cache | |
| run: | | |
| ~/.elan/bin/lake exe cache get || true | |
| rm -f ~/.cache/mathlib/*.ltar || true | |
| - name: Repo lint (TorchLean policies) | |
| run: ~/.elan/bin/lake lint | |
| - name: Build curated library surface | |
| run: ~/.elan/bin/lake build NN.Library | |
| - name: Cache API docs | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| .lake/build/doc/Aesop | |
| .lake/build/doc/Batteries | |
| .lake/build/doc/find | |
| .lake/build/doc/Init | |
| .lake/build/doc/Lake | |
| .lake/build/doc/Lean | |
| .lake/build/doc/Mathlib | |
| .lake/build/doc/Std | |
| key: Docs-${{ hashFiles('lake-manifest.json') }} | |
| - name: Build project API documentation | |
| run: | | |
| rm -rf .lake/build/doc-data .lake/build/api-docs.db | |
| DISABLE_EQUATIONS=1 ~/.elan/bin/lake -R -Kenv=dev build NN:docs | |
| - name: Detect homepage folder | |
| id: check_home_page | |
| run: | | |
| if [ -d home_page ]; then | |
| echo "The 'home_page' folder exists in the repository." | |
| echo "HOME_PAGE_EXISTS=true" >> $GITHUB_ENV | |
| else | |
| echo "The 'home_page' folder does not exist in the repository." | |
| echo "HOME_PAGE_EXISTS=false" >> $GITHUB_ENV | |
| fi | |
| - name: Build Verso guide (blueprint package) and copy to `home_page/blueprint` | |
| run: | | |
| cd blueprint | |
| ~/.elan/bin/lake exe cache get || true | |
| rm -f ~/.cache/mathlib/*.ltar || true | |
| ~/.elan/bin/lake exe blueprint-gen --output ../_out/blueprint | |
| cd .. | |
| if [ -d blueprint/TorchLeanBlueprint/Guide/Assets ]; then | |
| mkdir -p _out/blueprint/html-multi/Guide/Assets | |
| cp -r blueprint/TorchLeanBlueprint/Guide/Assets/* _out/blueprint/html-multi/Guide/Assets/ | |
| fi | |
| python3 scripts/docs/polish_verso_guide.py --guide _out/blueprint/html-multi | |
| rm -rf home_page/blueprint | |
| mkdir -p home_page/blueprint | |
| cp -r _out/blueprint/html-multi/* home_page/blueprint/ | |
| - name: Copy API documentation to `home_page/docs` | |
| run: | | |
| rm -rf home_page/docs | |
| cp -r .lake/build/doc home_page/docs | |
| python3 scripts/docs/polish_docgen.py --docs home_page/docs | |
| du -sh home_page/docs | |
| - name: Trim Lake build metadata from docs | |
| run: | | |
| find home_page/docs -name "*.trace" -delete | |
| find home_page/docs -name "*.hash" -delete | |
| - name: Reset generated manual output | |
| run: rm -rf home_page/manual | |
| - name: Build dependency graph audit | |
| run: | | |
| python3 scripts/checks/dependency_audit.py \ | |
| --root "$PWD" \ | |
| --json home_page/graphs/dependency-audit.json \ | |
| --markdown home_page/graphs/dependency-audit.md \ | |
| --fail-on-error | |
| - name: Build interactive import graph HTML | |
| run: | | |
| mkdir -p home_page/importgraph | |
| ~/.elan/bin/lake exe graph --to NN.Library home_page/importgraph/index.html | |
| python3 - <<'PY' | |
| from pathlib import Path | |
| page = Path("home_page/importgraph/index.html") | |
| html = page.read_text(encoding="utf-8") | |
| html = html.replace(' <link rel="stylesheet" href="style.css" />\n', "") | |
| html = html.replace( | |
| 'var docs_url = params.get("docs_url") || "https://leanprover-community.github.io/mathlib4_docs/";', | |
| 'var docs_url = params.get("docs_url") || new URL("../docs/", window.location.href).href;', | |
| ) | |
| page.write_text(html, encoding="utf-8") | |
| PY | |
| - name: Bundle dependencies | |
| uses: ruby/setup-ruby@v1 | |
| with: | |
| working-directory: home_page | |
| ruby-version: "3.0" | |
| bundler-cache: true | |
| - name: Build website using Jekyll | |
| if: env.HOME_PAGE_EXISTS == 'true' | |
| working-directory: home_page | |
| env: | |
| JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: JEKYLL_ENV=production bundle exec jekyll build | |
| - name: "Upload website (API documentation, blueprint and any home page)" | |
| if: github.event_name != 'pull_request' | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }} | |
| deploy_pages: | |
| runs-on: ubuntu-latest | |
| name: Deploy GitHub Pages | |
| needs: build_project | |
| if: github.event_name != 'pull_request' | |
| permissions: | |
| pages: write | |
| id-token: write | |
| environment: | |
| name: github-pages | |
| url: ${{ steps.deployment.outputs.page_url }} | |
| steps: | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v4 |