iterating on central files

Stream: general

[Greg Price]

What workflows do people use for working on changes to files in mathlib that lots of other things depend on?

I just tried adding a small definition to src/algebra/group/hom.lean, and the VS Code extension promptly stopped being able to show any information while the Lean server started doing a bunch of work, presumably recompiling everything else.

[Greg Price]

Sometimes for milder versions of this it's seemed to help if I go do leanproject build, producing a bunch of olean files, and then restart the server. So I tried that... but the build took:

time: 2071.967s wall (22081.312s u, 29.687s s)

about 35 minutes before it was done. (And total CPU time of 6 hours -- I'm quite grateful for Lean's parallel compilation.)

[Greg Price]

Experimenting a bit more, it looks like the VS Code extension is successful at getting fresh information quickly about the file I just edited itself.

The trouble is when I'm making a change there and I want to see the effect it has in some other file. I don't need to build the whole of mathlib just yet -- that can wait until a PR is nearly ready -- but just the very central file A that I just touched, and file B that I'm otherwise working in, and I guess the files that are between them in the import graph. Is there a way to do that?

[Floris van Doorn]

After changing a bunch of low level files, the usual workflow is

• create a new branch,
• push it to the remote repository (leanprover-community/mathlib)
• wait 0.5-3 hours (you can checkout other branches and work there)
• leanproject get-cache (on the commit you pushed) will download the compiled olean files generated by Github Actions. If there is an error in a later file, it will have compiled mathlib partially (but at least enough to compile the file that has an error).

[Floris van Doorn]

If you want to do it locally, you can do lean --make src/path/to/file.lean which will compile that file and everything it depends on

[Floris van Doorn]

in either case, run Lean: Restart in VSCode in order for the Lean server to use the newly generated olean files.

[Greg Price]

Floris van Doorn said:

If you want to do it locally, you can do lean --make src/path/to/file.lean which will compile that file and everything it depends on

That sounds like what I want, thanks!

[Greg Price]

The workflow using CI is also interesting. I guess it doesn't take any less time than my desktop can do it in, but could still be helpful when I want to be building something else at the same time.

[Greg Price]

That lean --make src/path/to/file.lean command has been very helpful already. Thanks again!

[Greg Price]

Often reduces the build time to just a few minutes.