After press ctrl+l ctrl+p or ctrl+l ctrl+n, we have error report in debug console:

Error: Invalid arguments
	at new l (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:87:21239)
	at new l (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:87:17220)
	at applyComputedTerm (/Users/claude/Downloads/projects/aya/aya-vscode/out/compute-term.js:21:24)
	at /Users/claude/Downloads/projects/aya/aya-vscode/out/features.js:24:152

I think the result passed to applyComputedTerm(...) is not in the right format, then I have no clue.

https://code.visualstudio.com/api/extension-guides/webview

It's stuck in this line

😟

The tutorial here https://www.aya-prover.org/guide/vscode-tutorial.html says to go to the aya-vscode github actions https://github.com/aya-prover/aya-vscode/actions/workflows/vsix.yml and to download the artifact from the latest successful run.

But when I try that the artifacts are already expired, since the last run was 2 months ago.

However, going to https://github.com/aya-prover/aya-vscode/releases/tag/nightly-build shows that there's the latest artifact available, the date of it matches the date of the latest run.

So maybe the docs can be updated to reflect this situation better.

As title

This is a feature request.

This is a feature request

I wanna implement a command like this:

• VSCode sends the LSP an instance of some subtype of org.eclipse.lsp4j.TextDocumentPositionParams (done in this client -- Idk how to do it, I need help!)
• LSP finds an instance of Doc (which, probably we need to convert to plain text before sending to VSCode, but maybe HTML also works?) and a range (done in the compiler, I know how to do it, I don't need help!)
• VSCode selects the provided range and show the Doc somehow, maybe similar to how GHC-Simple shows the type of expressions (done in this client -- Idk how to do it, I need help!)

@imkiva need your help!!

As title

VSCode shows notifications like “No definition found for ‘suc’”.

Related code: https://github.com/banacorn/agda-mode-vscode/blob/master/src/Highlighting.res#L87

It's very annoying to keep semantic tokens in sync with user edits manually. I decide to simply remove highlights when editing until we have a better way to update highlights as user types, or we just compromised.