Zulip Chat Archive

Stream: new members

Topic: command build a specific file


view this post on Zulip Anatole Dedecker (Aug 02 2020 at 22:02):

Sometimes when working on mathlib I need to add just a few lemmas to a really basic file (say data/set/intervals/basic) and then to work on a higher level file, e.g analysis/calculus/.... Usually, I just run leanproject build after modifying basic files, but the problem is this also compiles files I don't care, e.g category theory. Is there a command that would compile only files that 1) depend on a file that has been changed, which is what leanproject build does, and 2) are dependencies of a certain file, which is what the vscode extension does ?

In case you were wondering, here's why I can't just wait for VSCode to compile all necessary files : I'm on a laptop that doesn't have a lot of ram, and when coding I usually have quite a few or other tasks running, so I modified the allowed ram in vscode extension settings. But then lean can't handle compiling whole mathlib. On the other hand, when I do recompile it, I usually cut everything else, so I can run lean in CLI without any problems. This is a bit dirty but it should get better with more recent Linux kernels

view this post on Zulip Reid Barton (Aug 02 2020 at 22:09):

lean --make certainfile.lean

view this post on Zulip Anatole Dedecker (Aug 02 2020 at 22:11):

I totally should have tried that, but it turns out I'm dumb. Thanks !

view this post on Zulip Scott Morrison (Aug 03 2020 at 02:51):

Another option when working with limited computing resources is just to push your work to a non-master branch of the leanprover-community repo, and then use leanproject to retrieve the compiled olean files once they've been built by our continuous integration setup. It's not instant, but sometimes is a helpful solution.

view this post on Zulip Anatole Dedecker (Aug 03 2020 at 11:36):

Yep I do that sometimes too


Last updated: May 17 2021 at 22:15 UTC