From a9eab322d4ed10d1e7907239c3ea6436cc28edd6 Mon Sep 17 00:00:00 2001 From: dni Date: Fri, 30 Oct 2026 06:47:33 +0100 Subject: [PATCH] ci: add swap for the docs build and make it non-blocking doc-gen4 documents the whole import closure (Mathlib, VCVio, ...) and ran out of memory on the runner, failing the job although the proofs built. Add 16 GB of swap, only build docs on pushes to main, and let a docs failure not fail the job. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/lean_action_ci.yml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index db09247..70548d7 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -18,4 +18,19 @@ jobs: steps: - uses: actions/checkout@v5 - uses: leanprover/lean-action@v1 + # The API docs cover the whole import closure (Mathlib, VCVio, ...), and + # the runner's default 4 GB of swap is not enough for doc-gen4. + - name: Add swap for the docs build + if: github.event_name == 'push' && github.ref == 'refs/heads/main' + run: | + sudo swapoff -a + sudo rm -f /mnt/swapfile + sudo fallocate -l 16G /mnt/swapfile + sudo chmod 600 /mnt/swapfile + sudo mkswap /mnt/swapfile + sudo swapon /mnt/swapfile + free -h + # A docs failure should not mark the proofs as failing. - uses: leanprover-community/docgen-action@v1 + if: github.event_name == 'push' && github.ref == 'refs/heads/main' + continue-on-error: true