Zulip Chat Archive

Stream: general

Topic: cache in CI

Patrick Massot (Feb 24 2020 at 21:39):

Couldn't we use cache to help Travis. Say someone creates a PR. Travis could find the latest commit in the PR history which has an olean cache on Azure, git checkout that commit, get olean, git checkout the PR commit and try building. It wouldn't help with PRs touching tactic.core, but it should help a lot for PR extending maths in mathlib.

Scott Morrison (Feb 24 2020 at 21:42):

This would be great.

We should also switch to deciding to accept oleans via hash, rather than timestamp.

Last updated: Dec 20 2023 at 11:08 UTC