Zulip Chat Archive

Stream: general

Topic: iterating on central files


Greg Price (Apr 04 2021 at 00:48):

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 (Apr 04 2021 at 00:48):

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 (Apr 04 2021 at 00:55):

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 (Apr 04 2021 at 01:58):

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 (Apr 04 2021 at 02:00):

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 (Apr 04 2021 at 02:01):

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

Greg Price (Apr 04 2021 at 04:55):

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 (Apr 04 2021 at 05:01):

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 (Apr 04 2021 at 08:33):

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

Greg Price (Apr 04 2021 at 08:34):

Often reduces the build time to just a few minutes.


Last updated: Dec 20 2023 at 11:08 UTC