Fix live doc build by saving runner space

[kwankyu]

as seen in: https://github.com/sagemath/sage/actions/runs/9333677258/job/25690941738

📝 Checklist

• The title is concise and informative.
• The description explains in detail what this PR is about.
• I have linked a relevant issue or discussion.
• I have created tests covering the changes.
• I have updated the documentation and checked the documentation preview.

⌛ Dependencies

[github-actions]

Documentation preview for this PR (built with commit 2d56d27; changes) is ready! 🎉
This preview will update shortly after each push to this PR.

[mkoeppe]

Is there a test run already somewhere?

[kwankyu]

I ran it here: https://github.com/kwankyu/sage/actions/runs/9424396249 (second try). Let's see.

[kwankyu]

It works well.

[mkoeppe]

Then let's merge it.

[kwankyu]

Thanks!

[kwankyu]

I am confused by this: https://github.com/sagemath/sage/actions/runs/9357979101

That run succeeded in building live doc. Then this PR is not really needed...?

[kwankyu]

In particular, this step

      - name: Copy live doc
        id: copylivedoc
        if: (success() || failure()) && steps.buildlivedoc.outcome == 'success'
        run: |
          mkdir -p ./livedoc
          cp -r -L /sage/local/share/doc/sage/html ./livedoc
          cp -r -L /sage/local/share/doc/sage/pdf ./livedoc
          cp  /sage/local/share/doc/sage/index.html ./livedoc
          zip -r livedoc.zip livedoc
        shell: sh .ci/docker-exec-script.sh BUILD . {0}

worked as it is in the run. I thought this step would not work correctly because the commands run inside the docker container and hence create the file livedoc.zip inside the container, and the upload step fails because the zip file is not accessible. I am misunderstanding something. What is it?

[mkoeppe]

The container mounts the current directory (.) from the worker. These steps directly write to the worker file system.

[kwankyu]

I see. That explains it.

How about the space problem? Should we see the success of the last run as a sheer luck?

[mkoeppe]

It's better to save the space. It's clear that we are operating very close to the edge with our builds on these runners

[kwankyu]

I reviewed the last runs for from beta5 to beta8. Only the run for beta8 failed by lack of space.

It's better to save the space. It's clear that we are operating very close to the edge with our builds on these runners

OK. Thanks.