agda / agda-language-server Goto Github PK

View Code? Open in Web Editor NEW

96.0 9.0 17.0 372 KB

Language Server for Agda

License: MIT License

Haskell 100.00%

agda agda-mode language-server-protocol

agda-language-server's Introduction

Agda Language Server

Installation

The simplest way of acquiring Agda Language Server is through agda-mode on VS Code. Follow the instructions and the language server should be installed within seconds.

Prebuilt binaries

You can also download prebuilt binaries from the release page if you are using other LSP-compatible text editors.

Supported platforms: Windows, Mac, and Ubuntu.

Build from source

You will need Haskell Stack to build the project:

stack install

Versioning

The version is x.a.b.c.d.y where a.b.c.d is the 4-digit Agda version (2.6.4.0), x is 0 but may be bumped for revolutionary changes to the agda-language-server, and y is for patch releases.

Why make it standalone?

for less impact on the Agda codebase
to help decouple the Agda codebase
we can always merge it back to Agda later anyway

Hacking

This language server is co-developed alongside agda-mode on VS Code. Enable agdaMode.connection.agdaLanguageServer in agda-mode's settings, and then hit restart C-x C-r to connect to the language server. The editor extension will search for the language server in the following order:

localhost:4096 via TCP
als executable on your machine
Prebuilt binaries on GitHub

To host the language server locally at localhost:4096, run :main -p in the REPL (stack repl). This allows us to reload the language server in the REPL without having to recompile and reinstall the whole project on your system every time there is a change.

agda-language-server's People

Contributors

Stargazers

Watchers

Forkers

wldhx dannypsnl-fork archive-tsao-chi-forks lachrimae franklinchen vojtechstep ncfavier mildsunrise sno2wman emilienlemaire 4e554c4c sebeaumont lfrestrepog bodokat lllssskkk mrboboget zmrocze

agda-language-server's Issues

Usage with neovim

Has anyone used this with neovim? If so, can yall point me to instructions on how to set it up?

Problem with the locale of binaries built on GitHub Actions

If the source contains Unicode symbols like ⊤ in the example below:

module A where

data ⊤ : Set where 
  tt : {!   !}

The language server would crash with the following log output:

[Info] Starting server
[Debug] ---> {"jsonrpc":"2.0","id":0,"method":"initialize","params":{"processId":4012,"clientInfo":{"name":"Visual Studio Code","version":"1.84.2"},"locale":"en","rootPath":"/Users/banacorn/agda/examples","rootUri":"file:///Users/banacorn/agda/examples","capabilities":{"workspace":{"applyEdit":true,"workspaceEdit":{"documentChanges":true,"resourceOperations":["create","rename","delete"],"failureHandling":"textOnlyTransactional","normalizesLineEndings":true,"changeAnnotationSupport":{"groupsOnLabel":true}},"configuration":true,"didChangeWatchedFiles":{"dynamicRegistration":true,"relativePatternSupport":true},"symbol":{"dynamicRegistration":true,"symbolKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]},"tagSupport":{"valueSet":[1]},"resolveSupport":{"properties":["location.range"]}},"codeLens":{"refreshSupport":true},"executeCommand":{"dynamicRegistration":true},"didChangeConfiguration":{"dynamicRegistration":true},"workspaceFolders":true,"semanticTokens":{"refreshSupport":true},"fileOperations":{"dynamicRegistration":true,"didCreate":true,"didRename":true,"didDelete":true,"willCreate":true,"willRename":true,"willDelete":true},"inlineValue":{"refreshSupport":true},"inlayHint":{"refreshSupport":true},"diagnostics":{"refreshSupport":true}},"textDocument":{"publishDiagnostics":{"relatedInformation":true,"versionSupport":false,"tagSupport":{"valueSet":[1,2]},"codeDescriptionSupport":true,"dataSupport":true},"synchronization":{"dynamicRegistration":true,"willSave":true,"willSaveWaitUntil":true,"didSave":true},"completion":{"dynamicRegistration":true,"contextSupport":true,"completionItem":{"snippetSupport":true,"commitCharactersSupport":true,"documentationFormat":["markdown","plaintext"],"deprecatedSupport":true,"preselectSupport":true,"tagSupport":{"valueSet":[1]},"insertReplaceSupport":true,"resolveSupport":{"properties":["documentation","detail","additionalTextEdits"]},"insertTextModeSupport":{"valueSet":[1,2]},"labelDetailsSupport":true},"insertTextMode":2,"completionItemKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25]},"completionList":{"itemDefaults":["commitCharacters","editRange","insertTextFormat","insertTextMode"]}},"hover":{"dynamicRegistration":true,"contentFormat":["markdown","plaintext"]},"signatureHelp":{"dynamicRegistration":true,"signatureInformation":{"documentationFormat":["markdown","plaintext"],"parameterInformation":{"labelOffsetSupport":true},"activeParameterSupport":true},"contextSupport":true},"definition":{"dynamicRegistration":true,"linkSupport":true},"references":{"dynamicRegistration":true},"documentHighlight":{"dynamicRegistration":true},"documentSymbol":{"dynamicRegistration":true,"symbolKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]},"hierarchicalDocumentSymbolSupport":true,"tagSupport":{"valueSet":[1]},"labelSupport":true},"codeAction":{"dynamicRegistration":true,"isPreferredSupport":true,"disabledSupport":true,"dataSupport":true,"resolveSupport":{"properties":["edit"]},"codeActionLiteralSupport":{"codeActionKind":{"valueSet":["","quickfix","refactor","refactor.extract","refactor.inline","refactor.rewrite","source","source.organizeImports"]}},"honorsChangeAnnotations":false},"codeLens":{"dynamicRegistration":true},"formatting":{"dynamicRegistration":true},"rangeFormatting":{"dynamicRegistration":true},"onTypeFormatting":{"dynamicRegistration":true},"rename":{"dynamicRegistration":true,"prepareSupport":true,"prepareSupportDefaultBehavior":1,"honorsChangeAnnotations":true},"documentLink":{"dynamicRegistration":true,"tooltipSupport":true},"typeDefinition":{"dynamicRegistration":true,"linkSupport":true},"implementation":{"dynamicRegistration":true,"linkSupport":true},"colorProvider":{"dynamicRegistration":true},"foldingRange":{"dynamicRegistration":true,"rangeLimit":5000,"lineFoldingOnly":true,"foldingRangeKind":{"valueSet":["comment","imports","region"]},"foldingRange":{"collapsedText":false}},"declaration":{"dynamicRegistration":true,"linkSupport":true},"selectionRange":{"dynamicRegistration":true},"callHierarchy":{"dynamicRegistration":true},"semanticTokens":{"dynamicRegistration":true,"tokenTypes":["namespace","type","class","enum","interface","struct","typeParameter","parameter","variable","property","enumMember","event","function","method","macro","keyword","modifier","comment","string","number","regexp","operator","decorator"],"tokenModifiers":["declaration","definition","readonly","static","deprecated","abstract","async","modification","documentation","defaultLibrary"],"formats":["relative"],"requests":{"range":true,"full":{"delta":true}},"multilineTokenSupport":false,"overlappingTokenSupport":false,"serverCancelSupport":true,"augmentsSyntaxTokens":true},"linkedEditingRange":{"dynamicRegistration":true},"typeHierarchy":{"dynamicRegistration":true},"inlineValue":{"dynamicRegistration":true},"inlayHint":{"dynamicRegistration":true,"resolveSupport":{"properties":["tooltip","textEdits","label.tooltip","label.location","label.command"]}},"diagnostic":{"dynamicRegistration":true,"relatedDocumentSupport":false}},"window":{"showMessage":{"messageActionItem":{"additionalPropertiesSupport":true}},"showDocument":{"support":true},"workDoneProgress":true},"general":{"staleRequestSupport":{"cancel":true,"retryOnContentModified":["textDocument/semanticTokens/full","textDocument/semanticTokens/range","textDocument/semanticTokens/full/delta"]},"regularExpressions":{"engine":"ECMAScript","version":"ES2020"},"markdown":{"parser":"marked","version":"1.1.0"},"positionEncodings":["utf-16"]},"notebookDocument":{"synchronization":{"dynamicRegistration":true,"executionSummarySupport":true}}},"initializationOptions":{"commandLineOptions":[]},"trace":"off","workspaceFolders":[{"uri":"file:///Users/banacorn/agda/examples","name":"examples"}]}}
[Debug] <--2-- {"id":0,"jsonrpc":"2.0","result":{"capabilities":{"callHierarchyProvider":false,"codeActionProvider":false,"colorProvider":false,"declarationProvider":false,"definitionProvider":false,"documentFormattingProvider":false,"documentHighlightProvider":false,"documentRangeFormattingProvider":false,"documentSymbolProvider":false,"foldingRangeProvider":false,"hoverProvider":true,"implementationProvider":false,"referencesProvider":false,"renameProvider":false,"selectionRangeProvider":false,"semanticTokensProvider":{"legend":{"tokenModifiers":["declaration","definition","readonly","static","deprecated","abstract","async","modification","documentation","defaultLibrary"],"tokenTypes":["namespace","type","class","enum","interface","struct","typeParameter","parameter","variable","property","enumMember","event","function","method","macro","keyword","modifier","comment","string","number","regexp","operator"]}},"textDocumentSync":{"change":2,"openClose":true,"save":{"includeText":true},"willSave":false,"willSaveWaitUntil":f[aDlesbeu}g,]" t-y-p-e>D e{f"ijnsiotniropncP"r:o"v2i.d0e"r,"":mfeatlhsoed,"":w"oirnkistpiaaclei"z:e{d}",,""wpoarrkasmpsa"c:e{S}y}m
bolProvider":false}}}
[Debug] ---> {"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///Users/banacorn/agda/examples/A.agda","languageId":"agda","version":1,"text":"module A where\n\ndata als: <stderr>: hPutChar: invalid argument (invalid character)

Also, it seems like the are some concurrent interleaving problem with the logger.

Update `agda-language-server` on Hackage

I am currently trying to package this project for the Arch User Repository. This can (almost) be automated if there is an up-to-date version of the package on Hackage.

Would you consider releasing the newer versions of the language server there? Or is it a concious choice not?

Thank you in advance 👍

Expected functionality for non-VScode editors?

Hey @banacorn! I saw in another comment somewhere that this language server operates mostly on extensions spoken by both it and agda-mode (which makes sense as to much of the trouble I was having getting it working before).

I was wondering: could what is done via custom methods and what is done via standards be written down and made explicit somewhere? It is hard for me to know exactly what to expect out of this language server at the moment (and thus if it's working).

FTBFS on Debian

bss@monster % stack clean
bss@monster % stack build
Linking /home/bss/.stack/setup-exe-cache/x86_64-linux-tinfo6/tmp-Cabal-simple_6HauvNHV_3.2.1.0_ghc-8.10.7 ...

<no location info>: error:
    Warning: Couldn't figure out linker information!
             Make sure you're using GNU ld, GNU gold or the built in OS X linker, etc.
collect2: fatal error: cannot find ‘ld’
compilation terminated.
`gcc' failed in phase `Linker'. (Exit code: 1)

Error: [S-6374]
       While building simple Setup.hs (scroll up to its section to see the error) using:
       /home/bss/.stack/programs/x86_64-linux/ghc-tinfo6-8.10.7/bin/ghc-8.10.7 -rtsopts -threaded -clear-package-db -global-package-db -hide-all-packages -package base -main-is StackSetupShim.mainOverride -package Cabal-3.2.1.0 /home/bss/.stack/setup-exe-src/setup-6HauvNHV.hs /home/bss/.stack/setup-exe-src/setup-shim-6HauvNHV.hs -o /home/bss/.stack/setup-exe-cache/x86_64-linux-tinfo6/tmp-Cabal-simple_6HauvNHV_3.2.1.0_ghc-8.10.7
       Process exited with code: ExitFailure 1 
bss@monster % ld --version
GNU ld (GNU Binutils for Debian) 2.40
Copyright (C) 2023 Free Software Foundation, Inc.
This program is free software; you may redistribute it under the terms of
the GNU General Public License version 3 or (at your option) a later version.
This program has absolutely no warranty.
bss@monster % stack --version
Version 2.11.1, Git revision c1167a6abc3f4978ccded5ba0246a57387da0e2f x86_64 hpack-0.35.2
bss@monster % git status
On branch master
Your branch is up to date with 'github/master'.

nothing to commit, working tree clean
bss@monster % git rev-parse HEAD
d9525d5f5ab84df7408f68016714eb0e89ff71b8

Trying to use in nvim, like I do with hls.

I'm not exactly sure what the next step is, but I'd be glad to help.

I also got different errors trying to install it as a "binary dependency" inside another stack project using lts-19.33, but I figured the first step was to make sure I could checkout and compile the most recent version.

Connection Error

Hi,

After enabling the language server in VSCode agda-mode, I quit and restart. The language server downloads, but then the following is printed.

Connection Error: Client Internal Connection Error
Connection to server got closed. Server will not be restarted.

The debug output is

dyld: Library not loaded: /usr/local/opt/icu4c/lib/libicuuc.69.dylib
  Referenced from: /Users/<username>/Library/Application Support/Code/User/globalStorage/banacorn.agda-mode/v0.1.1-darwin/als
  Reason: image not found
[Error - 10:22:36 AM] Connection to server got closed. Server will not be restarted.

I do not have a /usr/local/opt folder (homebrew installs to /opt/homebrew). Is there a straightforward way to fix this? (btw agda-mode without LSP works just fine!)

Chris

Support semantic highlights

Agda is a very difficult language to parse.

Because of this, many other highlighting methods (such as textmate, or treesitter grammars) are not possible.

If the agda-language server supported semantic tokens, then many editors would be able to highlight agda code much better.

lsp: no handler for ...

I've been attempting to get als working with Helix's language server implementation. It seems to not recognize any of the events Helix is sending, though. Some selected events in Helix's log:

[INFO] als <- {"jsonrpc":"2.0","params":{"type":1,"message":"lsp:no handler for:  STextDocumentDidSave"},"method":"window/logMessage"}
[INFO] als <- {"jsonrpc":"2.0","params":{"type":1,"message":"lsp:no handler for:  STextDocumentDidChange"},"method":"window/logMessage"}
[INFO] als <- {"jsonrpc":"2.0","params":{"type":1,"message":"lsp:no handler for:  SInitialized"},"method":"window/logMessage"}
[INFO] als <- {"jsonrpc":"2.0","params":{"type":1,"message":"lsp:no handler for:  STextDocumentDidOpen"},"method":"window/logMessage"}
[INFO] window/logMessage: LogMessageParams { typ: Error, message: "lsp:no handler for:  STextDocumentDidClose" }

Would you happen to understand this error? I can't quite figure out if it's an issue with the editor I'm integrating this language server with or the language server itself. It's almost like the language server is passing over some serialized Haskell types, or something?

/nix/store/9j02mfzk6b490g9i3jl03ghzh4ydbvsy-standard-library-1.5/src/Data/Maybe.agda:11,1-33
/nix/store/9j02mfzk6b490g9i3jl03ghzh4ydbvsy-standard-library-1.5/_build:
createDirectory: permission denied (Read-only file system)

(CLI agda My.agda runs fine, agda-mode-vscode as well.)

NixOS installs a wrapper (see nixpkgs/build-support/agda/default.nix) for Agda:

    makeWrapper ${Agda}/bin/agda $out/bin/agda \
      --add-flags "--with-compiler=${ghc}/bin/ghc" \
      --add-flags "--library-file=${library-file}" \
      --add-flags "--local-interfaces"

while ALS apparently calls Agda directly as a library.

One solution would be to allow user to supply flags to call Agda with (the crucial one here being --local-interfaces).