leanprover / lean-action

GitHub action for standard CI in Lean projects
Apache License 2.0
16 stars 3 forks source link

Failed to save: Unable to reserve cache with key #96

Closed zhassan-aws closed 3 months ago

zhassan-aws commented 3 months ago

I'm seeing an error in the action log:

https://github.com/zhassan-aws/rust-lean-models/actions/runs/10584292641/job/29328218478#step:5:4

Error:

Post job cleanup.
Post job cleanup.
/usr/bin/tar --posix -cf cache.tzst --exclude cache.tzst -P -C /home/runner/work/rust-lean-models/rust-lean-models --files-from manifest.txt --use-compress-program zstdmt
Failed to save: Unable to reserve cache with key lake-Linux-0420ad22b402f1852b512085adf5f8f943dcbd2020c06b593dbf647109859e0f-cd723b8570f869ff062f20148a18904c204f7eaa53e3a01bd392f11cb7dbc66e-eea165edf99595c6e211834734719b7798198ce2, another job may be creating this cache. More details: Cache already exists. Scope: refs/heads/lean-action, Key: lake-Linux-0420ad22b402f1852b512085adf5f8f943dcbd2020c06b593dbf647109859e0f-cd723b8570f869ff062f20148a18904c204f7eaa53e3a01bd392f11cb7dbc66e-eea165edf99595c6e211834734719b7798198ce2, Version: 75b9baf94dc3418329547f553509d3a71e66f8fca8b8f11be0ccc25bd91684eb

This is the workflow file:

https://github.com/zhassan-aws/rust-lean-models/actions/runs/10584292641/workflow

Is the error expected?

It doesn't cause the action to fail though, which is good.

austinletson commented 3 months ago

Hi, thank you for opening an issue.

This duplicated cache saving behavior and corresponding error is caused by lean-action utilizing a combination of actions/cache (restores and saves cache) and actions/cache/save (just saves cache). I don't think this has a functional impact on the behavior of the lean-action, but it is inefficient and not ideal.

I have opened #97 to replace actions/cache with actions/cache/restore, which is more fitting and prevents unnecessary cache saving and will prevent this error moving forward.