Retrieving all diagnostics

Stream: lean4

[Jon Eugster]

It looks like lean4#3014 removed among other things Lean.Server.Snapshots.Snapshot.interactiveDiags and restructured quite a bit how snapshots work. @Sebastian Ullrich, could you maybe help me how to adjust the code snippet below, please? What is the correct way to retrieve all InteractiveDiagnostics inside RequestM?

In this snippet of v4.7.0 code, I want to simply collect all diagnostics of the entire file, and I'll need to update this code to v4.8.0 .

  withWaitFindSnap
    doc
    (fun snap => ¬ (snap.infoTree.goalsAt? doc.meta.text 0).isEmpty)
    (notFoundX := return none)
    fun snap => do
      let mut steps : Array <| InteractiveGoalsWithHints := #[]
      let mut diag : Array InteractiveDiagnostic := snap.interactiveDiags.toArray --error: does not exist anymore
      [...]

I've also skimmed the documentation Lean/Server.md and the release notes but didn't find any hints there.

[Sebastian Ullrich]

What is the context? Why can't you use the existing getInteractiveDiagnostics request?

[Jon Eugster]

the context is that NNG has a modified FileWorker which I was hoping to update and this is a custom builtinRpcProcedure collecting diags and goals at various places throughout the document. Your hint is definitely useful, but I wonder now since there are so many changes in v4.8.0 (and pressumably even more with the incremental compilation of v4.9.0), maybe it's not just a simple patch.

Maybe it's more reasonable to skip v4.8.0 and directly look into reimplementing that part in v4.9.0-rc1...

[Sebastian Ullrich]

No, all the changes on that front should already be in 4.8.0, no snapshot changes since then

[Sebastian Ullrich]

Jon Eugster said:

the context is that NNG has a modified FileWorker

Should I ask why? At least then it's not a surprise that updates will be painful

[Jon Eugster]

Ah ok, thats good to know. Thanks!

Tbh, I dont fully understand that part, @Alexander Bentkamp implemented that about 2 years ago and I tried to stay clear of it as much as possible:sweat_smile: But for example there is an extended WorkerState that also includes the game's data. The main two points are creating hints dependent of the proof step and blacklisting certain tactics/theorems. Another thing is that the user's editor only contains a tactic-proof, so that needs to be embedded into a theorem before elaborating.

But yes, maybe it's about time to look at that again... Maybe that would be a good question for one of these future FRO office hours, tobask what the conceptually best approach would be.

[Sebastian Ullrich]

I think my suggestion for something like that would have been to, in the client, transform the document such that the proof is embedded like you say and then, in the client again, shift all positions of requests and responses accordingly. All the game logic could then be done in a custom elaborator, e.g.

check_level "level1" := by
  <input>

[Alexander Bentkamp]

Maybe that would be easier, but maybe it's not. I don't think we can easily shift the requests and resonses or transform the document because those communications are handled by external packages on the client side (monaco-languageclient and lean4-infoview)

[Sebastian Ullrich]

It could also be a language server proxy that does the shifting, it would be like the watchdog but much simpler as it would not have to implement 1:n proxying

[Alexander Bentkamp]

Hm, that sounds better. The proxy would have to know all places where line info needs to be modified, but maybe thats ok.

[Alexander Bentkamp]

We probably still need a custom method to collect all goals along with the corresponding hints though. So it would not solve the particular problem that Jon raised, I think.