Use lake exe cache get to skip rebuilding Mathlib#7
Conversation
There was a problem hiding this comment.
Pull request overview
Updates the weekly indexing GitHub Actions workflow to leverage Mathlib’s Lake cache mechanism so the pipeline can avoid rebuilding Mathlib when possible.
Changes:
- Adds
lake exe cache getbeforelake buildin the PhysLib build step. - Reduces the PhysLib build step timeout from 90 minutes to 30 minutes.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| if: steps.check.outputs.has_changes == 'true' | ||
| run: cd physlib && lake build | ||
| timeout-minutes: 90 | ||
| run: cd physlib && lake exe cache get && lake build |
There was a problem hiding this comment.
The build step is now chained with &&, so any transient failure in lake exe cache get (network, cache server, missing artifact) will prevent lake build from running. If the intent is “use cache when available, otherwise fall back to building”, make cache get non-fatal (e.g., separate step or handle its exit code) so the workflow still proceeds to lake build.
| run: cd physlib && lake exe cache get && lake build | |
| run: | | |
| cd physlib | |
| lake exe cache get || echo "lake exe cache get failed; continuing with lake build" | |
| lake build |
| run: cd physlib && lake build | ||
| timeout-minutes: 90 | ||
| run: cd physlib && lake exe cache get && lake build | ||
| timeout-minutes: 30 |
There was a problem hiding this comment.
timeout-minutes was reduced from 90 to 30. If lake exe cache get is unavailable or the cache misses, the subsequent lake build may exceed 30 minutes and get killed even though it would succeed. Consider keeping a longer timeout (or making it conditional on cache-get success) to avoid flaky weekly runs.
| timeout-minutes: 30 | |
| timeout-minutes: 90 |
No description provided.