one click install of maths project

Stream: lean4

[Kevin Buzzard]

If I have a Lean 4 repo which depends on mathlib, is there a Lean 4 version of leanproject get my_name/my_repo which just downloads it from github and gets you a fully compiled Lean and mathlib and all the other shenannigans? I'm not asking for cached oleans for my own project files, just for mathlib and below.

[Scott Morrison]

@Kevin Buzzard, downstream repositories can run lake exe cache get, to retrieve mathlib oleans.