Stream: new members
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
Reid Barton (Aug 02 2020 at 22:09):
lean --make certainfile.lean
Anatole Dedecker (Aug 02 2020 at 22:11):
I totally should have tried that, but it turns out I'm dumb. Thanks !
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.
Anatole Dedecker (Aug 03 2020 at 11:36):
Yep I do that sometimes too
Last updated: May 17 2021 at 22:15 UTC