command build a specific file

Stream: new members

[Anatole Dedecker]

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

[Reid Barton]

lean --make certainfile.lean

[Anatole Dedecker]

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

[Scott Morrison]

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.

[Anatole Dedecker]

Yep I do that sometimes too