vscoq icon indicating copy to clipboard operation
vscoq copied to clipboard

Combine multi-message events into one larger event

Open Durbatuluk1701 opened this issue 1 year ago • 2 comments

The processing of a command such as debug auto on:

Lemma test : forall A B C : Prop,
  (A -> B) ->
  (B -> C) ->
  (A -> C).
Proof.
  debug auto.

yields the following in the language server debug log:

[lspManager          , 759167, 1724680109.787295] sent: {
  "params": {
    "diagnostics": [
      {
        "message": "(* debug auto: *)",
        "range": {
          "end": { "character": 13, "line": 30 },
          "start": { "character": 2, "line": 30 }
        },
        "severity": 3
      },
      {
        "message": "* assumption. (*fail*)",
        "range": {
          "end": { "character": 13, "line": 30 },
          "start": { "character": 2, "line": 30 }
        },
        "severity": 3
      },
     ...
     ...
     ...
      {
        "message": "*** assumption. (*success*)",
        "range": {
          "end": { "character": 13, "line": 30 },
          "start": { "character": 2, "line": 30 }
        },
        "severity": 3
      }
    ],
  },
  "method": "textDocument/publishDiagnostics",
  "jsonrpc": "2.0"
}

roughly 40 different messages from debug auto all pertaining to the same range and with the same severity

It might be nice and save some computation time if instead a single message/event was processed for commands that yield output related to a single range and with a single severity.

Durbatuluk1701 avatar Aug 26 '24 13:08 Durbatuluk1701

This additional API https://github.com/gares/sel/pull/16 should let one process feedback messages in batches.

It should be sufficient to use it here: https://github.com/coq/vscoq/blob/95068b803143cf1d9a32d18dc70c2a4b571a446c/language-server/dm/executionManager.ml#L422 and modify the type of LocalFeedback to carry a list of stuff, eg

type feedback = Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Quickfix.t list * Pp.t)
...
  | LocalFeedback of feedback Queue.t * feedback list

gares avatar Feb 12 '25 14:02 gares