build failing

Stream: FLT

[Kevin Buzzard]

The build is failing. Here's a link to the failure. I am merging PRs for which CI passes and then CI fails once they're merged. The error is

Run /home/runner/work/_actions/leanprover-community/docgen-action/deed0cdc44dd8e5de07a300773eb751d33e32fc8/scripts/build_docs.sh
  /home/runner/work/_actions/leanprover-community/docgen-action/deed0cdc44dd8e5de07a300773eb751d33e32fc8/scripts/build_docs.sh
  shell: /usr/bin/bash --noprofile --norc -e -o pipefail {0}
  env:
    LAKE_PACKAGE_DIRECTORY: .
    API_DOCS: true
    BUILD_ARGS: --log-level=warning
    DOCS_EXISTS: true
    NAME: FLT
    DOCS_FACETS: FLT:docs
    HOMEPAGE: docs
info: docbuild: no previous manifest, creating one from scratch
info: leanprover/doc-gen4: cloning https://github.com/leanprover/doc-gen4
info: leanprover/doc-gen4: checking out revision '8b1135b818a03f16d69fb796589ebb4ad448d5ea'
info: updating toolchain to 'leanprover/lean4:v4.26.0-rc2'
info: restarting Lake via Elan
info: docbuild: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
info: UnicodeBasic: cloning https://github.com/fgdorais/lean4-unicode-basic
info: UnicodeBasic: checking out revision '378b62cdf3bb90d3cd9aa12dc2be43b42bdda339'
error: external command 'git' exited with code 128
Error: Process completed with exit code 1.

I had imagined that it might be a transient network error but I reran a job and it didn't fix it, I merged another PR and it didn't fix it, so I'm now confused.

[Bryan Gin-ge Chen]

Probably this issue: #lean4 > UnicodeBasic: 'git' exited with code 128 (now fixed?)

[Aayush Rajasekaran]

@Kevin Buzzard Can you (or someone with the right perms) re-run the CI for this specific job (this is for the latest master, commit d7839af). I suspect that will work, since it should fetch the right commit for doc-gen4.

You'll know it did the right thing if line 2531, all the way at the end, changes from:
info: UnicodeBasic: checking out revision '378b62cdf3bb90d3cd9aa12dc2be43b42bdda339'
to:
info: UnicodeBasic: checking out revision '2679356b3372d52f76d6d984eef16cade7956e0c'

[Kevin Buzzard]

I tried rerunning the job and now got an exciting new error! The unicode version I got was
info: UnicodeBasic: checking out revision '106abeac8ee53a047b238976281b0e5017bded8a'
and then doc-gen seemed to work. But I got an error later on:

jekyll 3.9.5 | Error:  No space left on device - copy_file_range
/opt/hostedtoolcache/Ruby/3.1.7/x64/lib/ruby/3.1.0/fileutils.rb:1396:in `copy_stream': No space left on device - copy_file_range (Errno::ENOSPC)

[Kevin Buzzard]

So I don't know how to fix this. As far as I can see, what's happening is that the CI job

      - name: Upstreaming dashboard
        run: python3 scripts/upstreaming_dashboard.py

      - uses: leanprover-community/docgen-action@deed0cdc44dd8e5de07a300773eb751d33e32fc8 # 2025-10-26
        with:
          blueprint: true
          homepage: docs

in .github/workflows/blueprint.yml spends an hour building the FLT blueprint and when it's successfully done so, does this:

...
✔ [11555/11556] Built FLT/FermatsLastTheorem:docs (3.7s)
ℹ [11556/11556] Built FLT/FLT:docs (8.4s)
info: Documentation indexing
Build completed successfully (11556 jobs).
Run ruby/setup-ruby@eaecf785f6a34567a6d97f686bbb7bccc1ac1e5c
Modifying PATH
Downloading Ruby
  https://github.com/ruby/ruby-builder/releases/download/toolcache/ruby-3.1.7-ubuntu-24.04.tar.gz
  ENOSPC: no space left on device, write
  Waiting 12 seconds before trying again
  ENOSPC: no space left on device, write
  Waiting 11 seconds before trying again
  Took  23.85 seconds
Error: Error: ENOSPC: no space left on device, write

and that's the end of that.

Am I right in thinking that this leanprover-community/docgen-action is not a part of my project? I am just trying to get to grips with CI.

[David Renshaw]

Others have found that it can help to add a step to free up some disk space: https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/.22No.20space.20left.20on.20device.22/near/559142101

[David Renshaw]

leanprover-community/docgen-action tells Github how to build docs for your project.

[Kevin Buzzard]

Oh wow this is an entire _repo_?

I'm trying to learn something about CI this weekend -- thanks!

[David Renshaw]

I'm guessing that it downloads Ruby so that it can call jekyll to build your landing page.

[David Renshaw]

I'm preparing a PR for FLT to add the disk-clearing step that Pietro has successfully used elsewhere.

[David Renshaw]

https://github.com/ImperialCollegeLondon/FLT/pull/776

[Kevin Buzzard]

Thanks!

[Pietro Monticone]

Thank you @David Renshaw!