Skip to content

Conversation

Copy link
Contributor

Copilot AI commented Dec 17, 2025

The docker save step was failing with "no space left on device" when disk usage reached 91% (6.7GB available of 72GB total). System-level caches were accumulating before the save operation.

Changes

Added cleanup steps to remove system-level caches and uploaded artifacts:

  • After build tar.gz upload: Remove fiat-crypto-build.tar.gz from working directory
  • Before docker save: Remove /home/runner/.rustup (~600MB) and /home/runner/actions-runner/cached (~1.4GB)

Added enhanced diagnostics:

  • Fine-grained size reporting for rustup and actions-runner directories
  • Check for /dev/sdb1 mount status and write permissions
  • Disk space reporting via df -h before and after cleanup

Total space freed: ~2GB from system-level caches. Build artifacts in the working directory are preserved for use by subsequent jobs.

Original prompt

This section details on the original issue you should resolve

<issue_title>Coq dev docker sometimes runs out of disk space</issue_title>
<issue_description>Following up on #2218, I see

Run echo "=== Disk space usage ==="
=== Disk space usage ===
Filesystem      Size  Used Avail Use% Mounted on
/dev/root        72G   65G  6.7G  91% /
tmpfs           7.9G   84K  7.9G   1% /dev/shm
tmpfs           3.2G  1.2M  3.2G   1% /run
tmpfs           5.0M     0  5.0M   0% /run/lock
/dev/sda16      881M   62M  758M   8% /boot
/dev/sda15      105M  6.2M   99M   6% /boot/efi
/dev/sdb1        74G  4.1G   66G   6% /mnt
tmpfs           1.6G   12K  1.6G   1% /run/user/1001

=== Top 20 largest directories in current directory ===
6.8G	.
5.3G	./src
4.2G	./src/ExtractionOCaml
662M	./src/ExtractionHaskell
228M	./src/ExtractionJsOfOCaml
140M	./rupicola
130M	./rupicola/bedrock2
98M	./src/Bedrock
56M	./src/Util
47M	./src/Assembly
45M	./dist
41M	./rewriter

Build cache usage: 39.92kB

CACHE ID       CACHE TYPE     SIZE      CREATED       LAST USED     USAGE     SHARED
llsdzsutyu9r   regular        0B        2 hours ago   2 hours ago   1         true
8sep3ifwjiyq   regular        0B        2 hours ago   2 hours ago   1         true
u4rw32qf8zt8   regular        0B        2 hours ago   2 hours ago   1         true
x587776g9wgk   regular        0B        2 hours ago   2 hours ago   1         true
td7co6pdwnla   regular        0B        2 hours ago   2 hours ago   1         true
gpu4ndid48ws   regular        0B        2 hours ago   2 hours ago   1         true
mqzegm7vlidi   regular        0B        2 hours ago   2 hours ago   1         true
y2avnno30s0w   regular        0B        2 hours ago   2 hours ago   1         true
kp6fssgtnpfo   regular        0B        2 hours ago   2 hours ago   1         true
hx3fsfuxlc7b   regular        0B        2 hours ago   2 hours ago   1         true
1ygurasojbxo   regular        0B        2 hours ago   2 hours ago   1         true
ff4fs2cwo3sb   regular        0B        2 hours ago   2 hours ago   1         true
wy2uf0i6t1y7   regular        0B        2 hours ago   2 hours ago   1         true
vcq9fhc18hrj   regular        0B        2 hours ago   2 hours ago   1         true
px1d8qhx2h20   regular        0B        2 hours ago   2 hours ago   1         true
iglt3amczgoj   regular        594B      2 hours ago   2 hours ago   1         true
vyvum0h6nflm   source.local   149B      2 hours ago   2 hours ago   1         false
b6xfqxy1vice   source.local   61B       2 hours ago   2 hours ago   1         false
3mofi0s2rdh3   regular        0B        2 hours ago   2 hours ago   1         true
9ib0zk05dj54   source.local   39.7kB    2 hours ago   2 hours ago   1         false
d88oudfn4rc4   regular        0B        2 hours ago   2 hours ago   1         true
pdsr9r7ah4dz   regular        29.1kB    2 hours ago   2 hours ago   1         true
uilhw6veymaf   regular        10kB      2 hours ago   2 hours ago   1         true
2s
58s
Run docker save "$COQ_IMAGE" -o image.tar
write ./.docker_temp_939995876: no space left on device
Error: Process completed with exit code 1.
```</issue_description>

<agent_instructions>Do not delete anything in the docker image itself, but feel free to remove things in the ambient fs that will not be used by later steps.  Or if needed add more debugging printout.</agent_instructions>

## Comments on the Issue (you are @copilot in this section)

<comments>
</comments>


💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.

Copilot AI changed the title [WIP] Fix disk space issues in Coq dev docker Free disk space before docker save in coq-docker workflow Dec 17, 2025
Copilot AI requested a review from JasonGross December 17, 2025 03:16
@JasonGross
Copy link
Collaborator

@copilot Do not delete anything in . except for fiat-crypto-build.tar.gz. But you can delete things in rustup or actions-runner, do more fine-grained printout if you need to

=== Top 20 largest directories in /home/runner ===
8.8G	/home/runner
6.8G	/home/runner/work/fiat-crypto
6.8G	/home/runner/work
1.4G	/home/runner/actions-runner/cached
1.4G	/home/runner/actions-runner
600M	/home/runner/.rustup/toolchains
600M	/home/runner/.rustup
58M	/home/runner/.dotnet/tools
58M	/home/runner/.dotnet
26M	/home/runner/work/_actions
20M	/home/runner/.cargo/bin
20M	/home/runner/.cargo
3.2M	/home/runner/.nvm
1.9M	/home/runner/.nvm/test
784K	/home/runner/.nvm/.git
276K	/home/runner/.nvm/.github
128K	/home/runner/work/_temp
52K	/home/runner/.docker
40K	/home/runner/.docker/buildx
16K	/home/runner/work/_PipelineMapping

=== Docker images ===
REPOSITORY         TAG                                IMAGE ID       CREATED        SIZE
98a828             591ff58b7541407aa75b3bc4c7fbdf77   b24c88f92415   2 hours ago    369MB
rocq/rocq-prover   dev                                743a3b66e41d   19 hours ago   3.55GB

=== Docker system df ===
Images space usage:

REPOSITORY         TAG                                IMAGE ID       CREATED        SIZE      SHARED SIZE   UNIQUE SIZE   CONTAINERS
98a828             591ff58b7541407aa75b3bc4c7fbdf77   b24c88f92415   2 hours ago    369MB     0B            368.8MB       0
rocq/rocq-prover   dev                                743a3b66e41d   19 hours ago   3.55GB    0B            3.547GB       0

Containers space usage:

CONTAINER ID   IMAGE     COMMAND   LOCAL VOLUMES   SIZE      CREATED   STATUS    NAMES

Local Volumes space usage:

VOLUME NAME   LINKS     SIZE

Build cache usage: 39.92kB

Also what about seeing if you have permissions to write to /dev/sdb1 ?

Copy link
Contributor Author

Copilot AI commented Dec 17, 2025

@copilot Do not delete anything in . except for fiat-crypto-build.tar.gz. But you can delete things in rustup or actions-runner, do more fine-grained printout if you need to

=== Top 20 larg...

Updated in 8f1b127:

  • Removed deletions from current directory (only keeping fiat-crypto-build.tar.gz cleanup)
  • Added cleanup of /home/runner/.rustup (~600M)
  • Added cleanup of /home/runner/actions-runner/cached (~1.4G)
  • Added fine-grained diagnostics showing contents of rustup and actions-runner directories
  • Added check for /dev/sdb1 mount status and write permissions

Total space freed: ~2GB from system-level caches without touching build artifacts.

@JasonGross JasonGross force-pushed the copilot/fix-disk-space-issues branch from 8f1b127 to 7227edb Compare December 17, 2025 07:02
@JasonGross JasonGross marked this pull request as ready for review December 17, 2025 07:02
@JasonGross JasonGross enabled auto-merge (squash) December 17, 2025 07:02
@JasonGross JasonGross force-pushed the copilot/fix-disk-space-issues branch from 7227edb to 75c1128 Compare January 1, 2026 03:29
Copilot AI and others added 3 commits January 24, 2026 09:43
Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com>
…dback

Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com>
Comment out the removal of actions-runner cached files in the workflow.
@JasonGross JasonGross force-pushed the copilot/fix-disk-space-issues branch from 9ba4223 to dee78b5 Compare January 24, 2026 17:43
@JasonGross JasonGross disabled auto-merge January 24, 2026 19:25
@JasonGross JasonGross merged commit ce64075 into master Jan 24, 2026
18 of 32 checks passed
@JasonGross JasonGross deleted the copilot/fix-disk-space-issues branch January 24, 2026 19:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Coq dev docker sometimes runs out of disk space

2 participants