Should `lake` notice changes to (some?) environment variables when deciding whether to rebuild.

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.68k stars 421 forks source link

Should `lake` notice changes to (some?) environment variables when deciding whether to rebuild. #4297

Open kim-em opened 5 months ago

kim-em commented 5 months ago

I recently encountered a case where:

lake build          # fails
lake env lake build # fails, replaying the error from the previous build
lake clean
lake env lake build # succeeds, because the build cared about one of the environment variables set by `lake env`

I'm not sure what the desired behaviour is here. Perhaps lake should include the values of lean-relevant environment variables, and if these change trigger a rebuild?

kim-em commented 5 months ago

A related case is that there are Mathlib tactics that notice the CI enviroment variable, to do additional sanity checks during CI. However CI=true lake build locally is not reliable due to reuse.