disk space

Stream: Carleson

[Jeremy Tan]

@Floris van Doorn um…
Screenshot-from-2024-06-26-17-09-17.png
https://github.com/fpvandoorn/carleson/actions/runs/9676609250

[Jeremy Tan]

Is your computer out of space?

[Yaël Dillies]

No, it's a standard github runner, as seen from the error

[Floris van Doorn]

This is the CI that is failed, potentially related to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/clean.20up.20documentation.20directory

[Floris van Doorn]

I added a cleanup step that I found in the Mathlib CI, and that seems to have fixed the issue.

[Kim Morrison]

Floris van Doorn said:

I added a cleanup step that I found in the Mathlib CI, and that seems to have fixed the issue.

@Floris van Doorn, was this the

      - name: cleanup
        run: |
          find . -name . -o -prune -exec rm -rf -- {} +
          # Delete all but the 5 most recent toolchains.
          # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
          # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
          if cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"'; then
              : # Do nothing on success
          else
              : # Do nothing on failure, but suppress errors
          fi

step? If people are having to do this downstream, perhaps it it time for elan to add some support here so we don't end up with too many copies of this shell scripting nightmare. :-)

[Floris van Doorn]

Yes. Though I should note that only the first line actually did anything, I believe (I looked at one CI output, and it silently succeeded, but with the warning that ~/.elan/toolchains didn't exist).

[Floris van Doorn]

Oh, the cleanup was not a permanent solution, CI ran out of disk space again: https://github.com/fpvandoorn/carleson/actions/runs/9700051881

I have no idea what I'm doing with CI, and don't have time to investigate this in the next few days, so if anyone is willing to investigate / spot something stupid I do in the CI, please do!

[Jeremy Tan]

Since disabling Jekyll worked, and the website is static, I think you need to move the landing website https://florisvandoorn.com/carleson to a separate repository

[Jeremy Tan]

...as is done with the leanprover-community website

[Floris van Doorn]

Yes, that is probably a good idea. I'm still trying to figure out what is exactly happening. It is a website with literally 2 pages (the landing page and the 404 page), and I'm not sure why it should take up any significant amount of disk space.
Unless it's transforming all doc pages in some way...

[Yaël Dillies]

Surely it's also hosting the blueprint and the docs?

[Floris van Doorn]

Yes, but disabling Jekyll somehow fixes the disk space issue. But maybe that's just the "drop that overflows the bucket" as we say in Dutch (i.e. the straw that broke the camel’s back).

Have you ever encountered these spaces issues in LeanCamCombi, Yael?

[Yaël Dillies]

I think so, but it's almost two years ago now and I've fixed CI issues for three separate projects since then

[Floris van Doorn]

I've basically copied the CI from one of the repos you did the CI for (PFR, I believe), so I'm not sure what I'm doing wrong.

[Yaël Dillies]

Depends on how stringent you were with the copying. From experience, it is overwhelmingly easy to mess up copying an existing project (because an important file is in an unexpected directory, because there are github settings you don't see in the files, etc...)

[Floris van Doorn]

Ohhh... I have an idea: I'm deleting everything, and then fetching the cache, but I don't have the step

      - name: Make sure the cache works
        run: |
          mv docs/docs .lake/build/doc

which means that the cache never gets smaller, only bigger...

[Yaël Dillies]

Yep, looks like that could be it!

[Floris van Doorn]

If I just add that step, will thinks automatically work? I should probably also change something in Lean, so that I don't just fetch the existing (too large) cache?

[Yaël Dillies]

You could first try removing the cache-fetching step, let CI run once, then restore it... or simply change the name of the cache token to ensure your CI is not trying to fetch the old huge cache

[Floris van Doorn]

Btw, I tried the first option, but I'm still having this issue. I think I'm actually running out of disk space in my Github pages, not in the runner. The error consistently happens during the upload step.
And I actually have another project on my Github pages: https://github.com/fpvandoorn/BonnAnalysis/
and this one also started running into storage issues. I tried disabling some things there, but they didn't fix the issue in the Carleson project. And AFAIK Github offers no paid plan to increase storage space on Github pages...

[Floris van Doorn]

Does someone know how to clean / clear things in your Github pages? Or how to see what's on there?

[Pietro Monticone]

Opened PR fixing the disk space issue.