Caching .o files in a Github workflow

Stream: general

[Geoffrey Irving]

https://github.com/girving/ray-render has a Github workflow https://github.com/girving/ray-render/blob/main/.github/workflows/lean.yml which unfortunately takes a long time due to the need to build 2.5k .o files, even if nothing has actually changed. https://github.com/girving/ray-render/actions/runs/17009507360/job/48223623672 is an example of a run.

Anyone have an example of a workflow that caches .o files too, to make rebuilds faster?

[Bryan Gin-ge Chen]

I don't know of anything specific to lean, but you could try using https://github.com/actions/cache

[Sebastian Ullrich]

lean-action already does this https://github.com/leanprover/lean-action?tab=readme-ov-file#caching-lake-directory-with-githubs-actionscache

[Geoffrey Irving]

Wonderful, lean-action is great! The workflow time went from 14 minutes to 1.5 minutes. :)