When an open file is changed, also update diagnostics and other IDE state for dependent files

[keyboardDrummer]

Background

Currently the Dafny IDE considers each opened file separately, even when one open file depends on another one. The IDE keeps separate state and runs a separate compilation for each opened file.

Related issue: dafny-lang/ide-vscode#82

Change

When any file is changed in the IDE, any open files that depend on the changed file will be included in the compilation, so resolution and verification are updated not just for the changed file but also of those files.

Not in scope

• A Dafny project file
• Change mechanisms to prevent one error from cascading into many, which might occur when the error occurs in something that has dependencies.

Prerequisites

• Cache module resolution in the LSP server #2330
• Cache Boogie translation and preprocessing at the Dafny module level #2361
• Cache verification in the LSP server #2331
• On change, only cancel compilation tasks whose inputs have changed #2332

Implementation suggestions

• For an implicit Dafny project, record which files are accessed through module imports. If any file is opened that was accessed in an existing implicit Dafny project, add that file to it.
• A change in any file in an implicit Dafny project causes the entire project to be recompiled.

[cpitclaudel]

When any file is changed in the IDE, any open files that depend on the changed file will be included in the compilation, so resolution and verification are updated not just for the changed file but also of those files.

I wonder if there's a way for us to do this but reduce the noise from resolution errors in other files. I worry that any change to a file that that breaks its own resolution will cause a flurry of resolution errors in other files (which, if we're not careful, will also invalidate their caches).

Maybe it's possible to delay the checking of other files if the current one doesn't resolve, at least by a bit.

[keyboardDrummer]

When any file is changed in the IDE, any open files that depend on the changed file will be included in the compilation, so resolution and verification are updated not just for the changed file but also of those files.

I wonder if there's a way for us to do this but reduce the noise from resolution errors in other files. I worry that any change to a file that that breaks its own resolution will cause a flurry of resolution errors in other files (which, if we're not careful, will also invalidate their caches).

Maybe it's possible to delay the checking of other files if the current one doesn't resolve, at least by a bit.

It can be as simple as not resolving a module until all its dependencies resolve without errors, although I think that might be too strict. Maybe we can distinguish between internal and external module errors, and stop resolution of dependents if there are external module errors.

I've marking this out of scope for this issue, since if this is an issue, it occurs on the CLI right now already so I think it's fine to also have it in the IDE.

[cpitclaudel]

It can be as simple as not resolving a module until all its dependencies resolve without errors, although I think that might be too strict.

Indeed, for example if we rename a constructor it's nice to all files that use it

I've marking this out of scope for this issue

👍

[keyboardDrummer]

Closing this issue because we won't do this. If no project file is used, editing a file will not update the diagnostics of files that depend on the edited file, even if they are also open in the IDE.