VSCode does not display results of ctrl-C, ctrl-L or ctrl-C, ctrl-P

[jxxcarlson]

VSCode is not working reliably with adga-mode. I have an up-to-date copy and am using Agda version 2.6.1.1-fce01db.

My experience of today: VSCode worked normally for a few hours, then misbehaved as described in the title. I know that type-checking for works for ctrl-C, ctrl-L because of the presence/absence of syntax coloration. However, no message is displayed, which is bad when there is a syntax error.

It was suggested that I "restart" VSCode, which I did by quitting, then re-opening the file. This worked a few times but no longer works. I've tried opening files that worked fine and that I did not touch today. VSCode misbehaves as described with them as well.

[GetContented]

@jxxcarlson it works much better if you install the latest version of agda, but I understand you're probably wanting to use 2.6.1.1 because of PLFA, like me. Just thought I'd let you know.

[slemus9]

@jxxcarlson I had the same issue. I found out that, after you re-open vscode, sometimes an empty window pane appears at the bottom of the screen (this is where agda-mode should output its results). Try to close that empty pane and then restart vscode - after doing this, the extension worked as expected for me.

If you didn't close the agda-mode's output window in your previous session, that empty window appears again when you re-open vscode (at least in my case). Hope this helps.

[GetContented]

Try to close that empty pane and then restart vscode - after doing this, the extension worked as expected for me.

I've noticed for a long time this seems to be a general VSCode issue — if there are pending updates waiting to be applied, VSCode does things like this. I suppose I should report it, or at least check it's been captured as an issue :-)