mit-plv
Free disk space before docker save in coq-docker workflow
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.gzfrom 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/sdb1mount status and write permissions - Disk space reporting via
df -hbefore 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 mit-plv/fiat-crypto#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>
- Fixes mit-plv/fiat-crypto#2222
💡 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 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 ?
@copilot Do not delete anything in
.except forfiat-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.gzcleanup) - 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/sdb1mount status and write permissions
Total space freed: ~2GB from system-level caches without touching build artifacts.