oleans from fork

Stream: general

[Robert Maxton]

Am I correct that, in order to let github do the annoying "recompile half of mathlib if you edit a file early in the import tree" bit and generate oleans for you to fetch with lake exe cache get, we now just need to

• Open the fork
• Enable workflows
• Push your commit?

[Bryan Gin-ge Chen]

The oleans won't be stored in the cloud cache unless you create a PR to mathlib4; pushing a commit is not enough. Also, you don't need to enable workflows on your fork (most of them will be disabled anyways).

[Robert Maxton]

Ah, I see, so it's still mathlib4 that does the building. Thanks!