agda-mode-vscode icon indicating copy to clipboard operation
agda-mode-vscode copied to clipboard

Loading can fail silently

Open joliss opened this issue 2 years ago • 1 comments

There are cases where loading an Agda file with C-c C-l can fail silently, without any error message or indication that something went wrong. I managed to reproduce it in the following way:

  1. In VS Code, open an Agda project with an Agda file.
  2. Load the file with C-c C-l. This should work.
  3. Go to settings and changeagdaMode.connection.agdaPath to /does/not/exist.
  4. Quit VS Code without closing the current window by pressing Cmd+Q on Mac.
  5. Re-open VS Code. It restores the project window.
  6. Press C-c C-l. This fails without an error message.

Here's a screenshot showing what my window looks like after step 7:

generic-syntax 2022-05-22 17-22-18

This might seem like an obscure corner case, but I think there are more cases where this happens -- this is just one way that I managed to reproduce it. I've had this behavior a bunch while trying to get Agda running for the first time, and it was a source of confusion for me.

joliss avatar May 22 '22 16:05 joliss

Thank you for this detailed step-by-step reproduction!

In step 5, after opening the editor, you should see a black panel like in the screenshot. If you close that blank panel, step 6. should work.

VS Code used to "reuse" that blank panel so everything would appear normal, but now VS Code has changed its behaviour recently, and I'm not sure if it's possible to restore this.

banacorn avatar May 29 '22 06:05 banacorn