leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
3.88k stars 329 forks source link

Lake: `--old` doesn't seem to work #2822

Closed Kha closed 2 weeks ago

Kha commented 7 months ago
$ lake new foo; cd foo; lake build
[0/6] Building Foo.Basic
[1/6] Compiling Foo.Basic
[1/6] Building Foo
[2/6] Compiling Foo
[2/6] Building Main
[3/6] Compiling Main
[6/6] Linking foo
$ echo >> Foo.lean; lake build --old
[2/6] Building Foo
[3/6] Compiling Foo
[3/6] Building Main
[4/6] Compiling Main
[6/6] Linking foo

Main should not be rebuilt here.

Kha commented 6 months ago

Funnily enough lake build actually does the minimum amount of rebuilds in this synthetic example. Should --old still look at hashes when they tell us a file does not have to be rebuilt? I.e. so lake build --old never builds more than lake build.