Locally making lean

Stream: lean4

[Wrenna Robson]

When I am working on a PR to core, and I want to start on it, is there a quicker way to get a working copy of a build then building it locally? I often find this can take more than an hour and it's quite tiresome to do every time. I don't think there's any caching system, is there: or am I missing something?

[Kim Morrison]

script/build_artifact.py

[Wrenna Robson]

Oh! Thank you.

[Wrenna Robson]

@Kim Morrison I don't actually see that script in the repo

[Wrenna Robson]

At least not in my local copy... but I do on github. Weird.

[Wrenna Robson]

Oh I got it.

[Wrenna Robson]

Hmm. Having run this script, when opening src/Init/Nat/Bitwise/Lemmas.lean I get "unexpected token 'where'; expected command" as an error on line 503 and 506

[Wrenna Robson]

That is having opened vs code with "code lean.code-workspace"

[Wrenna Robson]

Having made an edit to a file in Init, how do I best quickly recompile so that I can use my changes in a file later in the hierarchy?

[Kim Morrison]

Just the usual make -j -C build/release .

[Wrenna Robson]

Righto