RFC: Automatic file reloading when dependencies change

[hgoldstein95]

Proposal

I'd like a setting that always calls "Restart Lean server for file" in open editor tabs when their dependencies change. Sometimes I'm working on one file Foo.lean with a library function/tactic and another Bar.lean that calls that function/tactic. It'd be nice if I could have a mode where I didn't need to manually open Bar.lean and run the "Restart Lean server for file" action to see if my change in Foo actually had the intended effect.

This has been a frustration for me for a while, but it's especially annoying for me now that I'm playing around with using an AI agent to edit code — the agent often reads LSP output from a file I haven't reloaded in a while and concludes that a change it made didn't work, even though the issue is really just that the file needs to be reloaded.

Concretely:

• User Experience: Simplifies user workflow when working on multiple files that depend on one another, especially with the help of automated tools.

• Beneficiaries: All Lean users who wish to split their code across files.

• Maintainability: I could imagine a world where this is just default behavior, in which case it doesn't seem more or less maintainable. As a setting, I suppose it does add one more thing to maintain / test.

Community Feedback

This was discussed in this thread.

[mhuisi]

I have some further questions about this RFC:

1. Do you expect dependent files to be restarted only when the file you are looking at is saved, or automatically after a change has been made?
2. Do you only expect to see errors for open editor tabs, or for files that have not been opened as editor tabs as well? (I.e.: do you expect a full rebuild of the entire project, or only for the files that are currently open as tabs?)
3. Are you confident that your AI agent will correctly interpret the set of diagnostics produced by the language server once dependent files are being reloaded automatically?
   (I'm asking because we've heard reports in the past that AI agents will not use the correct set of diagnostics even when looking at a single file, since LSP was not designed with AI agents in mind and there is no standardized way for push-diagnostics to designate themselves as being the "complete" set of diagnostics for the fully elaborated file that an AI agent should use, as opposed to one from the partial elaboration states)

For historical context, it's perhaps worth pointing out that Lean 3 used to work similarly to what you describe and that many users actively requested it to be changed because Lean rebuilds generally tend to be quite expensive, and triggering a full rebuild of the entire project can take a very long time (now even more so than in Lean 3 because Lean projects are now much larger). Even just rebuilding the modules in all open tabs and all of their dependencies can be very problematic, as users often have "stale" tabs sitting around that they opened at some point in the past and are currently not actively using, i.e. "tabs" don't necessarily correspond closely to "active working set".
Especially in Mathlib, if you change some leaf file, a full rebuild after the fact can take hours on slower machines in the worst case until you can start working again, so I am very skeptical of the idea to make this the default in the current formulation - I can only ever imagine this being useful in small projects where rebuilds are always cheap.

[hgoldstein95]

1. On save, on change would be too much rebuilding.
2. The behavior I'm used to from other languages is often to show errors in unopened files too, but I could see either behavior making sense.
3. No, I'm not. I've wanted to be able to work efficiently between dependent files in Lean for a while now, so I'd be happy with this feature even if it doesn't actually fix the interaction with the agent. But at least having this setting would make Lean the same as other languages in that interaction loop.

I appreciate the context. I think part of the assumption I'm making here (which I guess isn't quite right) is that we can rebuild only dependencies of the current file, not all files that it depends on. In my ideal world, changing a leaf file in Mathlib would trigger no rebuild at all, since nothing depends on it. And when I change a file with a lot of dependencies, I sort of do want to know how all of the files that depend on it on might have broken, not just the ones I decided to click on and check.

At the end of the day, I mostly just don't want to feel like Lean is pushing me towards a workflow where I don't break up my code properly. Right now the experience of editing code in a single file is much nicer than trying to edit across files. And in some domains (e.g., Mathlib) I appreciate that might be worthwhile tradeoff to avoid the cost of rebuilding everything. It's just a bit of a shame in other use-cases.

[mhuisi]

But at least having this setting would make Lean the same as other languages in that interaction loop.

It unfortunately won't. In most other languages, diagnostics are only reported when the full module has been processed (which would be horrible for Lean), and so the issue just doesn't arise in the first place, as there is always only a single set of reported diagnostics per document version.

In my ideal world, changing a leaf file in Mathlib would trigger no rebuild at all, since nothing depends on it.

When I say "leaf file", what I mean is a file that is very deep in the import hierarchy, i.e. a file that is imported by lots of files :-) I guess this is not the standard way to think about the graph.

And when I change a file with a lot of dependencies, I sort of do want to know how all of the files that depend on it on might have broken, not just the ones I decided to click on and check.

I don't think that this is universally true. In some cases, you want to know about all the places that break (i.e. in our current workflow you'd just run lake build and wait), while in other cases, you just want to work on two or more specific modules for now and propagate changes between them as quickly as possible without paying in terms of latency or hardware utilization for modules that you currently do not care about. In most languages, you don't really have to pay much of a price for just always propagating every change through to the entire project because semantic analysis is always comparatively cheap, but this is unfortunately not true for Lean (due to meta-programming, proof automation, etc.).

At the end of the day, I mostly just don't want to feel like Lean is pushing me towards a workflow where I don't break up my code properly. Right now the experience of editing code in a single file is much nicer than trying to edit across files.

I agree and also strongly dislike the current overly manual workflow that we've converged to, but I think it's also worth pointing out that even when these rebuilds happen automatically and were to be limited to the exact working set that you currently want to be kept in sync, working in separate modules may still end up being more painful than working in the same module purely due to the fact that semantic analysis is expensive in Lean: when you initiate a rebuild on your dependent module, you always have to re-build at least the dependency that you changed in full from the top (and all of the modules between the two modules, at least provided that the new module system is not being applied carefully yet, which has some other additional implications for friction). If your modules are sufficiently slow (e.g. minutes per module, as can sometimes be the case in large Lean projects), then this latency on its own can create an incentive to move code that is often edited together closer together.

[mhuisi]

One potential idea to make these things a bit nicer that I've had in the past is to have a separate UI in VS Code that allows you to configure the actual working set of modules in your tabs that you want to be kept in sync automatically, so that you don't have to constantly pay for rebuilds in tabs that you opened at some point in the past and then forgot about. Selecting no modules results in the current manual workflow and selecting multiple modules means that selected dependents are automatically rebuilt when saving a module. I believe Isabelle has something similar to this in jEdit, too.

But it's not entirely clear to me yet what that UI would look like, or how we can best fit it into the default layout so that it is pleasant to use on smaller screens :-)