Repository navigation
Incremental build cache can cause incorrect test results #13449
Description
Activity
Yes, please fix this as it is a serious latent soundness issue. We love lean and are building great things on it.
Reacted by Robin Salkeld- added a commit that references this issue
on Apr 21, 2026 If your tests depend on additional data outside the Lean file you can specify this in Lake and Lake will trigger a rebuild when this additional content changes. For example:
lakefile.lean
input_dir testsTexts where path := "tests/texts" filter := .extension "txt" text := true input_file testsBlob where path := "tests/data.blob" @[test_driver] lean_lib FooTests where needs := #[testsTexts, testsBlob] -- ...
lakefile.toml
testDriver = ["FooTests"] [[input_dir]] name = "testsTexts" path = "tests/texts" filter.extension = ["txt"] text = true [[input_file]] name = "testsBlob" path = "tests/data.blob" [[lean_lib]] name = "FooTests" needs = ["testsTexts", "testsBlob"] # ...
Thanks for the information @tydeu! This sounds like potentially a decent partial workaround for now, if we can also set up a mechanism to ensure that all such files in the project are declared as input. Are the
input_dirandinput_filedeclarations documented somewhere? I didn't see mentions of them in https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/I stand by the assertion that the root cause still needs a solution though. Even assuming we create the mechanism above, that's something that every Lean project would have to create independently. It's also not going to be a bullet-proof solution for tests that execute external tools that don't live inside the project directory.
@robin-aws Lake operates on the assumption that Lean modules in libraries have their inputs fully specified. If you want to run an arbitrary mixture of tools on every
lake test, you can use anlean_exeorscripttest driver instead. For example:lakefile.lean
@[test_driver] script test do IO.println s!"Runs on every `lake test`: {← IO.monoMsNow}" return 0
lakefile.toml
testDriver = ["tester"] [[lean_exe]] name = "tester" root = "TestMain"
Yes I also considered defining a test runner instead. We already have have a large test library written, so it would need to be something that both builds Lean modules and executes other less pure testing. It still means ensuring that the testing Lean modules remain IO-free over time, so I would still feel the need for more of a mechanism to ensure that.
Lake operates on the assumption that Lean modules in libraries have their inputs fully specified.
Understandable, but I'm not yet clear on how a Lean project can ensure that assumption is true in practice.
I do think the simplest quick solution would be for
leanprover/lean-actionto not share the.lakedirectory as a cache across commit SHAs by default. It's fine if we want to say thatlakeis similar tomakein that you have to correctly specify all the dependencies manually, but most projects don't rely on the correctness of incremental builds in CI, so the consequences of getting them wrong are much smaller.I do think the simplest quick solution would be for
leanprover/lean-actionto not share the.lakedirectory as a cache across commit SHAs by default. It's fine if we want to say thatlakeis similar tomakein that you have to correctly specify all the dependencies manually, but most projects don't rely on the correctness of incremental builds in CI, so the consequences of getting them wrong are much smaller.As I understand, there is option on
leanprover/lean-actionto configure this:use-github-cache: "false". This just defaults to"true"because, as you noted, it is suitable for most projects (as they do not have such build complexities).Yup, and we've already disabled the default caching on our CI, and started customizing the cache keys to include the external files. But we had several instances of confusion and wasted time on incorrect CI builds before getting to that point, and we've now disabled most cache reuse between builds because it wasn't clear how to quickly be able to trust it again. If we weren't worried about backwards compatibility I'd just advocate for the default
use-github-cachevalue to be "false", and for the action's documentation to say "hey you should consider turning on caching, but just make sure all your dependencies are declared correctly!"I will investigate what options might work for making the user experience better and safer here without breaking anyone.
There is also a key misconception in the original issue I want to correct:
Lean is already so strict about tracking all side-effects of evaluation
This is not really true. Lean does no tracking of the "real world" side effects of elaboration/evaluation (e.g., reads from the filesystem or environment variables). The primary thing that it does carefully track is the Lean environment (e.g., logical definitions, information for metaprogramming). The ability of elaboration to perform arbitrary I/O is why comparator (the trusted judge of Lean code) elaborates solutions in a sandboxed environment.
Usually, Lean programs do not depend on data outside the Lean environment, and Lake assumes this as well. Should users desire this, it is expected they will inform Lake of this (either using builtin utilities or custom build scripts) or implement manual workarounds outside of Lake (such as clearing the build directory).
That's fair, I was trying to say that as a programming language, Lean is very strict about explicitly modeling side effects in the type system (and I edited the issue description to clarify). This led me to believe that checking if elaboration of a file might perform I/O would be reducible to a type checking problem. I can't claim to understand the details of elaboration and I can appreciate that dynamically tracking side effects isn't tractable, but that's not what I was imagining.
Usually, Lean programs do not depend on data outside the Lean environment, and Lake assumes this as well. Should users desire this, it is expected they will inform Lake of this (either using builtin utilities or custom build scripts) or implement manual workarounds outside of Lake (such as clearing the build directory).
I think as Lean adoption grows it will probably become more common, although I still suspect you're right that it will still be the minority. Can you see an easy way to ensure users are more aware of this expectation? The best experience would be if the tooling blocked you from adding these dependencies without declaring them in
lakefile.toml.BTW I very much appreciate the responses and information here. I'm a big fan of Lean so far and I'm being a pain about this issue because I worry about it negatively affecting the perception of Lean. ❤️
Can you see an easy way to ensure users are more aware of this expectation? The best experience would be if the tooling blocked you from adding these dependencies without declaring them in
lakefile.toml.There has been some talk of having a builtin sandboxed mode (e.g., via a
--sandboxflag) for Lake builds and Lean elaboration (on platforms that could support it). The discussion thus far had been focused on security, but detecting undeclared build requirements could be another use case. I think this is good motivation for us to consider that further. Np promises on anything soon, though.BTW I very much appreciate the responses and information here. I'm a big fan of Lean so far and I'm being a pain about this issue because I worry about it negatively affecting the perception of Lean. ❤️
Thank you for the kind words! ❤️🙏
Reacted by Emilio Jesús Gallego AriasThere has been some talk of having a builtin sandboxed mode (e.g., via a --sandbox flag) for Lake builds and Lean elaboration (on platforms that could support it). The discussion thus far had been focused on security, but detecting undeclared build requirements could be another use case. I think this is good motivation for us to consider that further. Np promises on anything soon, though.
Nice! is there an issue for that I could +1 and follow?
I'll pursue my type-checking approach idea and see if it pans out.
Nice! is there an issue for that I could +1 and follow?
Unfortunately, no. The discussion was never recorded as an issue (as far as I am aware).
I think a script is likely the right answer here, but I have wondered if lake could support dynamic dependencies similar to shake.
The mechanism would probably be a Lean environment extension that allowed custom elaborators to register that they read from a file (and thus it should be checked in determining rebuilds). The custom elaborator could also record "no cache" to indicate that while being built, it decided
lakeshouldn't cache the results (useful if a test was skipped).@joehendrix Lake does support dynamic dependencies (in custom targets) -- this is what Lake's
fetchis. In fact,fetchwas inspired by Shake's design. However, finding the right approach to support this in modules is difficult. What you are suggesting is similar to #2762, which I eventually choose to handle by implementingneedsandinput_file/input_dir. In the future, I would like to see it possible to declare additional dependencies through the module header as well (e.g., through specialimports), but that has not yet become a FRO priority.@tydeu How about an persistent environment extension that allowed registering additional dependencies?
Then when checking whether to use a previously built olean, you can read the additional dependencies out of the extension and check if they have been updated since the olean was built.
@joehendrix Unfortunately, it is not possible to import multiple environments in parallel. Thus, it is not possible to read oleans from within Lake's build monitor.
Separately, this would only consistently work for dependencies which do not, themselves, need building. For example, if a new required dynamic dependency A is added to module M, this would not be know until after module M is built. However, in order for the build to succeed, dependency A needs to be built, but this is not known without building M. Thus, a dependency cycle emerges and a proper build is impossible.
As far as I understood the discussion, the issue itself is not something we want to change per se but various solutions to the same effect have been discussed. I will close this issue then in favor of future ones focused on such a solution but let me know if that doesn't make sense.
Yes that's just fine for now thanks. I've got a deeper solution for this in the works (strata-org/Strata#1061) but it's not polished yet. I would love Lean expert feedback on it once it is though, so I may reopen this later if it makes sense.
Prerequisites
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
Lake incremental building does not consider external sources of input, and therefore a cached
.lakedirectorycan cause incorrect test results.
Context
It is common to implement tests in a Lean project by direct evaluation of test expressions using commands such as
#guard_msgsand#eval. This allows for a simple approach where tests are written in Lean source files in a separate directory, andlake testjust builds these files.However,
lakealso supports incremental building by recording a trace file of dependencies and output when building a module, and if the Lean source files involved in elaboration haven't changed, the trace is just replayed instead of actually re-building the source. Elaboration can depend on external state, for example via an#evalcommand where the argument is a monad instance that reads from non-Lean files. The effect is that changing these other forms of input and rebuilding just replays the previous result, even if the true result has gone from passing to failing.This is made more serious by the fact that the Lean ecosystem encourages sharing
.lakecontent between builds and even between projects. The default behavior of the leanprover/lean-action GitHub action, for example, is to save and restore the.lakedirectory between builds. This means these incorrect results can easily happen in CI as well, which means it's possible for a project's main branch to appear green when in reality doing a fresh build reveals that it is broken.Steps to Reproduce
See https://github.com/robin-aws/LeanCachingBug for a live example of this going wrong in a GitHub repository. It was created using
lake init, and the GitHub actions configuration was checked in unmodified.mainbranch contains a Lean test with parameterized data read from a text file. It passes both in CI and in a local clone.To reproduce locally:
lake build. It should succeed.2, 2, 5to the end ofAdditionTestData.txt.lake buildagain. It succeeds, incorrectly.rm -rf .lake.lake buildagain. This time it should fail, with a message oferror: CalculatorTest.lean:13:0: Failed: 2 + 2 != 5Expected behavior:
Build results from Lean source files with elaboration that depends on external state should not be replayed incorrectly. Either by recording enough information to ensure that replaying the trace is sound, or by giving up and rebuilding instead of replaying if the results may be incorrect.
Actual behavior:
Build results are replayed as long as the actual transitive Lean source has not changed.
Versions
4.29.1
Additional Information
I certainly understand that it's normally very hard to avoid any issue with stale cached build results. ("There are only two hard problems in computer science: cache invalidation, naming things, and off-by-one errors" :) I debated whether this should be phrased as an RFC instead. But I believe this is actually relatively easy and critical to solve in Lean's case, for two reasons:
#evalwhere the argument is one of the supported monad types. This can be refined over time for specific cases such asIO.FS.readFile, where the target can be recorded as additional input in the trace, the hashes include the content of the file etc. But this would just be additional performance optimization and not necessary to be sound.Impact
I noticed this issue in the context of the https://github.com/strata-org/Strata Lean-based project. I created this PR to partially disable the cache to avoid this issue, but it's definitely going to slow down the merge queue and hence development, as well as not addressing the issue of confusing stale local builds. Addressing this issue would give us, and many other Lean users, a lot more confidence to add deep integration tests to the native build and test process.