reservoir update frequency and toolchain version

Stream: lean4

[Eric Wieser]

I just converted a package of mine to Lean 4, but I don't yet see it on https://reservoir.lean-lang.org/; is there any live updating in place at the moment, or are we just looking at a preview snapshot? If the former, is there any requirement beyond having a lakefile.lean at the root of the repo?

[Eric Wieser]

I also note that https://reservoir.lean-lang.org/ says that it is using leanprover/lean4:v4.2.0-rc1; I assume this is just further evidence we are looking at a preview snapshot?

[Utensil Song]

Reservoir runs CI on push or workflow_dispatchand filters the repos with star >1 and a lakefile.lean etc. Last run on Oct 13 .

[Scott Morrison]

Yes, reservoir is just an early prototype at the moment!

Adding a cron job to update the "latest" toolchain is on @Mac Malone's todo list, but so are many other things. :-)