RFC: Automatic file reloading when dependencies change

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.

Start by reviewing the existing VS Code action named “Restart Lean server for file” and the linked Zulip discussion about automatically updating downstream files. Define how the proposed setting should detect dependency changes and which open editor tabs it should reload; done means dependent files update without manually invoking the action.