Lean docgen build error when deploying to website

Stream: general

[Fred Rajasekaran]

I get the following error when trying to build my project using Github workflows: jekyll 3.9.2 | Error: No space left on device - copy_file_range (line 14849 in here). Has anyone else experienced this issue/know a fix? I'm not too familiar with Jekyll/if this is an error with docgen or something else, so any help is appreciated. For reference, the workflow that is running is here

[Ruben Van de Velde]

Possibly similar issue reported here: #FLT > build failing @ 💬

[Jz Pan]

Same problem here: https://github.com/acmepjz/lean-iwasawa/actions/runs/20097667484/job/57660067292#step:4:6015. Fixed by manually re-run the workflow.

[Pietro Monticone]

@Fred Rajasekaran Opened PR to fix the issue.

[Pietro Monticone]

@Jz Pan Opened PR to fix the issue.

[Ruben Van de Velde]

Do we have a template that we could put this into?

[Pietro Monticone]

Doing it right now.

[Pietro Monticone]

Opened LeanBlueprint PR to fix the issue upstream.

[Fred Rajasekaran]

Thanks @Pietro Monticone ! The fix worked