Interactive mode

[ranjitjhala]

Add a FLUX_CHECK_DIFF=1 mode which

• tracks the modification time for each DefId's source file,
• only checks those DefId that belong to source files that were modified after the last check time
• OR (unfortunately) DefId that generated refinement errors when last checked.

[ranjitjhala]

@nilehmann I updated this PR with the relevant stuff for the vscode extension too.

@Samir-Rashid If you want to merge in your edits, the key bit would be to ensure that the TypeEnvTrace::new(...) generates TypeEnvBind where the loc field is a "nice" string (e.g. source-level name like x, y, z) instead of a flux-internal thing like _1, _2, _3 etc.

[ranjitjhala]

(or @Samir-Rashid -- as I said, just merge in your source-map stuff in a separate PR, and we can then merge the two...)

[nilehmann]

@ranjitjhala can you split the vscode bits into a separate PR. I have no problem merging that, but I have apprehensions about FLUX_CHECK_DIFF. I still think the extension should be the one telling flux what to check instead of flux trying to infer a diff that's simply going to be wrong.

[ranjitjhala]

@nilehmann the catch with getting the extension to tell flux which file to check is that I can't think of some easy way to actually do so. The only way (?) seems to be changing the ENV variables? which seems difficult as you have to change the "override-command" for each run?

At any rate, it doesn't really matter if the diff is wrong -- to be sound, you just run without the diff mode.

[ranjitjhala]

To be clear: the difficulty is just in "communicating" the relevant files to flux -- the extension already tracks the set internally.

[nilehmann]

If we have an extension we don't need to rely on rust analyzer running flux.

The way I see this working is that the extension implements a command (that you can run through the command palette or with keyboard shortcut) that calls cargo flux passing the necessary context. I was thinking we can pass the file and cursor position and then flux can infer the DefId from that. How we pass the context is not that important since we have full control of the invocation, it can be env vars or command flags.

Note that this is independent from having rust analyzer run flux. We can let rust analyzer run flux and show errors and the extension calling flux to get the checker trace. In the future, we can have the extension do both, for that we would need to implement a mapping between the error format in flux and vscode.

[ranjitjhala]

hmm seems a bit wasteful to run flux twice (its neat we can reuse rust-analyzer for the errors, pretty pointless to replicate it) -- but let me try it!

[nilehmann]

I don't have numbers, but I've experienced measurable slowdowns just by enabling the trace dump because it is too verbose, especially if we are dumping into a file. So what's also wasteful is to dump the trace on functions that you are not going to inspect. I'm trying to remove that overhead by not dumping the trace by default. If you don't dump the trace by default and then want to inspect a function, you actually want to re-run flux to produce the trace. But we can reduce that to a single function (modulo some stuff that we do on every run like parsing, the check diff also doesn't fix this though).

The one thing that could be considerably expensive to re-run is fixpoint, especially because we don't cache negative queries and presumably you'd want to inspect functions that do not verify. The reason we don't cache negative results is that we keep some state in memory to map the tags on heads back to info that we can use to report errors. But now I'm thinking that we can also cache negative queries by hashing that state and making it part of the "input". We just need to be careful with that hash being stable across compilations because it has spans, but rustc already implements some notion of stable hashing we could reuse.

[ranjitjhala]

One hassle with caching negative queries IMO is you need to _also_ save the errors (otherwise they will mysteriously disappear...)

…

On Tue, Dec 3, 2024 at 12:01 PM Nico Lehmann ***@***.***> wrote: I don't have numbers, but I've experienced measurable slowdowns just by enabling the trace dump because it is too verbose, especially if we are dumping into a file. So what's also wasteful is to dump the trace on functions that you are not going to inspect. I'm trying to remove that overhead by not dumping the trace by default. If you don't dump the trace by default and then want to inspect a function, you actually want to re-run flux to produce the trace. But we can reduce that to a single function (modulo some stuff that we do on every run like parsing, the check diff also doesn't fix this though). The one thing that could be considerably expensive to re-run is fixpoint, especially because we don't cache negative queries and presumably you'd want to inspect functions that do not verify. The reason we don't cache negative results is that we keep some state in memory to map the tags on heads back to info that we can use to report errors. But now I'm thinking that we can also cache negative queries by hashing that state and making it part of the "input". We just need to be careful with that hash being stable across compilations because it has spans, but rustc already implements some notion of stable hashing we could reuse. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/flux-rs/flux/pull/914*issuecomment-2515435051__;Iw!!Mih3wA!HYldbpBozH5KVMvD-rqmwBIJSzcBQDoi-SkKvGaqTunsCubNxz3RvEDYuEtt60rgnshHx45EDbVyk8mwrpdxuR2t$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OH4JVR52NXNH7B5RNL2DYEYDAVCNFSM6AAAAABS4USHL6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKMJVGQZTKMBVGE__;!!Mih3wA!HYldbpBozH5KVMvD-rqmwBIJSzcBQDoi-SkKvGaqTunsCubNxz3RvEDYuEtt60rgnshHx45EDbVyk8mwrix4Q-3l$> . You are receiving this because you were mentioned.Message ID: ***@***.***>

-- - Ranjit.

[ranjitjhala]

subsumed by #919 #917