Cache for PhysLean and projects downstream of Mathlib

Stream: general

[Joseph Tooby-Smith]

I just had a conversation with @Kenny Lau, and we were talking about the practicalities of setting up a cache for PhysLean (and therefore by extension projects downstream of Mathlib), and what that would involve.

This led to two questions:

• Is it possible to set up a cache without a server, using e.g. github artifacts?
• Are there any examples of projects downsteam of Mathlib that have done this?

The aim is just to make a cache of the master branch of the project, to speed up local builds, and github workflows.

[Ruben Van de Velde]

I'm not aware of anyone having done it, but it does sound useful. I'm not sure if the FRO has ideas on integrating things into reservoir that could replace the cache

[Yaël Dillies]

I believe the recent switch to contributions from forks was made possible by the (exact?) same advances one would need to set cache up for a downstream project

[Kim Morrison]

@Mac Malone, perhaps you could field this one, and summarize the state of your plans?

[Mac Malone]

Lake itself has plans to have a builtin Mathlib-style cache. However, that is planned to support Mathlib-style server setups and Reservoir version-based integration. It sounds like you would like a Mathlib-style setup without the server, which is not a use case we are currently focused on.

Lake also currently supports a serverless full-package cache that makes use of GitHub releases. ProofWidgets uses this. However, that would not cover your master branch aim.

Joseph Tooby-Smith said:

• Is it possible to set up a cache without a server, using e.g. github artifacts?

GitHub artifacts are temporary (they last for at most 90 days iirc), so they are often not a good fit for cache. However, if you are only trying to reuse recent builds, that may work well. You can store the .lake directory in an artifact and retrieve it in GitHub Actions or locally with GitHub CLI. If the uses are expected to be comfortable with a bit of manual command-line work in this regard, this may be the best option.

[Joseph Tooby-Smith]

Ok, many thanks for the info @Mac Malone ! I will see if I can get the artifacts to work, I don't think the 90 days limit will be an issue.

[Arthur Paulino]

You can also copy Mathlib's Cache and adapt it to your needs (i.e. changing some hardcoded parts and the request logic)

[Kim Morrison]

I think the right approach here is to plan to have a server, and use the upcoming lake replacement of Mathlib's cache.

[Kim Morrison]

Presumably we'll provide simple instructions for the hosting (which doesn't require a real server, just cloud storage). Ideally you could then do it yourself, and we can discuss solutions to the costs if you're not able to cover that elsewhere.

[Kim Morrison]

Artifact based solutions are likely going to remain a hacky distraction: Mac is building the right solution for you.

[Joseph Tooby-Smith]

Ok, thanks Kim, I'll sit tight and wait then.