Zulip Chat Archive

Stream: general

Topic: CI example

Yury G. Kudryashov (May 23 2023 at 21:57):

Hi, do we have an example github actions configuration file for a Lean 3 project? It should install Lean 3 & tools, call leanproject get-mathlib, then build the project.

Eric Wieser (May 23 2023 at 22:25):

It's not the one recommended by our webpage, but I recommend https://github.com/eric-wieser/lean-graded-rings/blob/master/.github/workflows/lean_build.yml

Eric Wieser (May 23 2023 at 22:25):

That one caches oleans on GitHub, which speeds up sequential builds

Yury G. Kudryashov (May 23 2023 at 23:08):

Can I download oleans built by this CI?

Eric Wieser (May 24 2023 at 03:52):

Not easily

Last updated: Dec 20 2023 at 11:08 UTC