Zulip Chat Archive

Stream: general

Topic: iterating on central files


view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Greg Price (Apr 04 2021 at 08:33):

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

view this post on Zulip Greg Price (Apr 04 2021 at 08:34):

Often reduces the build time to just a few minutes.


Last updated: May 14 2021 at 00:42 UTC