search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

"interpret to next with no observe_id" after editing the first sentence #925

Open tomtomjhj opened 6 days ago

tomtomjhj commented 6 days ago

vscoqtop crashes when user checks the first sentence of a document, edits it, and step forward.

The following is tested with coq vesion 8.19.2, vscoq-language-server 2.2.1, default settings, with both the official vscode client and my neovim client.

Reproduction steps

Make a file with the following content.

Definition F (q w e r t y u i o p : nat) : nat := q + w + e + r + t + y + u + i + o + p.

Step forward to check the definition of F: image

Delete the q parameter of F: image

Attempt to step forward, then vscoqtop crashes and restarts: image

Logs from "vscoq.args": [ "-bt", "-vscoq-d", "all" ]

Here are some parts of the log that I think are significant:

vscoqtop initializes and parses the document:

[lspManager          , 1521082, 1728110880.677768] Received notification: textDocument/didOpen
[document            , 1521082, 1728110880.710514] Parsing more from pos -1
[document            , 1521082, 1728110880.710527] Start of parse is: 0
[document            , 1521082, 1728110880.710927] Parsed: Definition F (q w e r t y u i o p : nat) : nat :=
  q + w + e + r + t + y + u + i + o + p.
[document            , 1521082, 1728110880.710970] Start of parse is: 88
[document            , 1521082, 1728110880.710982] 1 new sentences
[document            , 1521082, 1728110880.710988] 0 new comments
[document            , 1521082, 1728110880.710994] Top edit: 0, Doc: , Doc by id: 
[document            , 1521082, 1728110880.711000] diff:
+ [Definition--F--(--q--w--e--r--t--y--u--i--o--p--:--nat--)--:--nat--:=--q--+--w--+--e--+--r--+--t--+--y--+--u--+--i--+--o--+--p--.]
[lspManager          , 1521082, 1728110880.711042] sent: {
  "params": {
    "uri": "file:///path/to/file.v",
    "preparedRange": [],
    "processingRange": [],
    "processedRange": []
  },
  "method": "vscoq/updateHighlights",
  "jsonrpc": "2.0"
}

vscoqtop receives the first stepForward notification:

[lspManager          , 1521082, 1728110884.813374] UI req ready
[top                 , 1521082, 1728110884.813428] Main loop event ready: Request , 2 events waiting
[lspManager          , 1521082, 1728110884.813443] Received notification: vscoq/stepForward
[executionManager    , 1521082, 1728110884.813456] Non (locally) computed state 2
[lspManager          , 1521082, 1728110884.813580] sent: {
  "params": {
    "uri": "file:///path/to/file.v",
    "preparedRange": [
      {
        "end": { "character": 88, "line": 0 },
        "start": { "character": 0, "line": 0 }
      }
    ],
    "processingRange": [],
    "processedRange": []
  },
  "method": "vscoq/updateHighlights",
  "jsonrpc": "2.0"
}
[top                 , 1521082, 1728110884.813769] Main loop event ready: ExecuteToLoc 2 (1 tasks left, started 0.000 ago) , 4 events waiting
[executionManager    , 1521082, 1728110884.814616] --------- Prepared ranges ---------
[executionManager    , 1521082, 1728110884.814628] -------------------------------------
[executionManager    , 1521082, 1728110884.814631] --------- Processing ranges ---------
[executionManager    , 1521082, 1728110884.814638] -------------------------------------
[executionManager    , 1521082, 1728110884.814648] --------- Processed ranges ---------
[executionManager    , 1521082, 1728110884.814666] Range (start: (0,0), end: (0,88))
[executionManager    , 1521082, 1728110884.814672] -------------------------------------
[lspManager          , 1521082, 1728110884.814758] sent: {
  "params": {
    "uri": "file:///path/to/file.v",
    "preparedRange": [],
    "processingRange": [],
    "processedRange": [
      {
        "end": { "character": 88, "line": 0 },
        "start": { "character": 0, "line": 0 }
      }
    ]
  },
  "method": "vscoq/updateHighlights",
  "jsonrpc": "2.0"
}

/* bunch of duplicate "vscoq/updateHighlights" */

[top                 , 1521082, 1728110884.815296] Main loop event ready: proofview , 3 events waiting
[documentManager     , 1521082, 1728110884.815312] get_messages: Found id
[lspManager          , 1521082, 1728110884.815320] -------------------------- sending proof view ---------------------------------------
[lspManager          , 1521082, 1728110884.815401] sent: {
  "params": {
    "proof": null,
    "messages": [
      [
        3,
        [
          "Ppcmd_glue",
          [ [ "Ppcmd_string", "F" ], [ "Ppcmd_string", " is defined" ] ]
        ]
      ]
    ]
  },
  "method": "vscoq/proofView",
  "jsonrpc": "2.0"
}

vscoqtop receives didChange:

[top                 , 1521082, 1728110904.965704] Main loop event ready: Request , 2 events waiting
[lspManager          , 1521082, 1728110904.965728] Received notification: textDocument/didChange
[documentManager     , 1521082, 1728110904.965757] APPLYING TEXT EDIT Range (start: (0,14), end: (0,15)) []
[document            , 1521082, 1728110904.965779] Parsing more from pos -1
[document            , 1521082, 1728110904.965786] Start of parse is: 0
[document            , 1521082, 1728110904.966256] Parsed: Definition F (w e r t y u i o p : nat) : nat :=
  q + w + e + r + t + y + u + i + o + p.
[document            , 1521082, 1728110904.966335] Start of parse is: 87
[document            , 1521082, 1728110904.966356] 1 new sentences
[document            , 1521082, 1728110904.966363] 0 new comments
[document            , 1521082, 1728110904.966383] Top edit: 0, Doc: [Definition--F--(--q--w--e--r--t--y--u--i--o--p--:--nat--)--:--nat--:=--q--+--w--+--e--+--r--+--t--+--y--+--u--+--i--+--o--+--p--.], Doc by id: [Definition--F--(--q--w--e--r--t--y--u--i--o--p--:--nat--)--:--nat--:=--q--+--w--+--e--+--r--+--t--+--y--+--u--+--i--+--o--+--p--.]
[document            , 1521082, 1728110904.966399] diff:
- (id: 2) [Definition--F--(--q--w--e--r--t--y--u--i--o--p--:--nat--)--:--nat--:=--q--+--w--+--e--+--r--+--t--+--y--+--u--+--i--+--o--+--p--.]
+ [Definition--F--(--w--e--r--t--y--u--i--o--p--:--nat--)--:--nat--:=--q--+--w--+--e--+--r--+--t--+--y--+--u--+--i--+--o--+--p--.]
[executionManager    , 1521082, 1728110904.966419] Invalidating: 2
[lspManager          , 1521082, 1728110904.966517] sent: {
  "params": {
    "uri": "file:///path/to/file.v",
    "preparedRange": [],
    "processingRange": [],
    "processedRange": [
      {
        "end": { "character": 87, "line": 0 },
        "start": { "character": 0, "line": 0 }
      }
    ]
  },
  "method": "vscoq/updateHighlights",
  "jsonrpc": "2.0"
}
[lspManager          , 1521082, 1728110904.966580] sent: {
  "params": {
    "diagnostics": [],
    "uri": "file:///path/to/file.v"
  },
  "method": "textDocument/publishDiagnostics",
  "jsonrpc": "2.0"
}

vscoqtop receives the second stepForward and crashes:

[lspManager          , 1521082, 1728110949.063774] UI req ready
[top                 , 1521082, 1728110949.063834] Main loop event ready: Request , 2 events waiting
[lspManager          , 1521082, 1728110949.063850] Received notification: vscoq/stepForward
[top                 , 1521082, 1728110949.063862] ==========================================================
[top                 , 1521082, 1728110949.063934] Uncaught exception Failure("interpret to next with no observe_id").
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Dune__exe__LspManager.coqtopStepForward in file "vscoqtop/lspManager.ml", line 446, characters 38-105
Called from Dune__exe__LspManager.handle_lsp_event in file "vscoqtop/lspManager.ml", line 656, characters 22-49
Called from Dune__exe__Vscoqtop.loop.loop in file "vscoqtop/vscoqtop.ml", line 28, characters 21-50
Called from Dune__exe__Vscoqtop.loop in file "vscoqtop/vscoqtop.ml", line 33, characters 6-15

[top                 , 1521082, 1728110949.063945] ==========================================================
[Error - 3:49:09 PM] Server process exited with code 0.
[Info  - 3:49:09 PM] Connection to server got closed. Server will restart.

No crash when editing non-first sentences

Make a file with the following content

Definition F1 (q w e r t y u i o p : nat) : nat := q + w + e + r + t + y + u + i + o + p.
Definition F2 (q w e r t y u i o p : nat) : nat := q + w + e + r + t + y + u + i + o + p.

Check up to second setennce, and delete the q parameter from F2.

In this case, the check part retracts properly, and stepping forward does not crash. image

possible fix

It seems that editting the first sentence sets observe_id to None, which triggers the crash here. https://github.com/coq-community/vscoq/blob/f13ff1a9f252dc6ac3386e10215605ebec194cae/language-server/dm/documentManager.ml#L381

I believe observe_id should be set to Some Top instead.