Zulip Chat Archive

Stream: general

Topic: leanproject get-cache: get outdated

Mario Carneiro (Mar 23 2021 at 02:09):

Currently, if the latest commit of a PR is in progress, leanproject up becomes somewhat self-defeating, because it always pulls to get the latest version even if that commit doesn't have a cache. Would it be possible to modify the behavior so that it gets the last version that has a cache? It should also set the remaining files as dirty so that lean knows to compile them, if necessary (I think this is automatic).

Bryan Gin-ge Chen (Mar 23 2021 at 02:38):

This was also suggested here. (I haven't had time to work on this.)

Last updated: Aug 03 2023 at 10:10 UTC