agda 2.6.4 #22
agda 2.6.4 #22
Conversation
`explainWhyInScope` was not exported by `Agda` until 2.6.3, so it had to be duplicated.
| @@ -77,21 +83,29 @@ library | |||
| , base >=4.7 && <5 | |||
| , bytestring | |||
| , containers | |||
| , lsp <1.7 | |||
| , lsp <2 | |||
| , lsp-types <2 | |||
There was a problem hiding this comment.
Maybe I should keep this at < 1.7.
| #if MIN_VERSION_Agda(2,6,4) | ||
| GoalAndHave expr bndry -> do | ||
| -- TODO: render bndry | ||
| #else |
There was a problem hiding this comment.
@banacorn: Here I do not really know how to render the boundary. It would be good to be able to test the output before releasing some rendering. How would one test this?
There was a problem hiding this comment.
Let me see if I can release a new version of agda-mode on the VS Code Marketplace so that you can test this with ease!
There was a problem hiding this comment.
I've just released agda-mode v.0.4.4!
To test the language server:
- Build and install the language server on your machine so that
alsis in PATH - Enable
agdaMode.connection.agdaLanguageServerin the settings - Load an Agda file with
C-c C-l - If all goes well, you should see "ALS-2.6.4" on the top right corner of the panel.
.
You should also see errors likeLSP: no handler for: STextDocumentDidOpenpopping up.
There was a problem hiding this comment.
I've found the reason why there's this TCP tunneling thing on the server. It allow us to develop the language server right in the REPL without having to recompile and reinstall it.
See https://github.com/agda/agda-language-server#hacking for more.
| | isNoName (unqualify x) = | ||
| vcat ["where", vcat $ fmap render ds] | ||
| render (AnyWhere _range ds) = vcat ["where", vcat $ fmap render ds] | ||
| #if MIN_VERSION_Agda(2,6,4) | ||
| render (SomeWhere _range _er m a ds) = |
There was a problem hiding this comment.
I am currently ignoring erasure annotations but I suppose they should be rendered.
andreasabel
force-pushed
the
agda-2.6.4
branch
from
b00a86f
to
ccfa2a3
Compare
|
agda-mode v.0.4.6 just released! To test the language server: Build and install the language server on your machine so that als is in PATH |
…ntDidChange notifications
… this is the last one we need)
Agda.TypeChecking.Error.explainWhyInScopeshowInfoErrorfromEmacsToprather than duplicating it here