REPL?

[michaelmesser]

Microsoft considers REPL out of scope for LSP, but that doesn't mean we can't implement it anyways. This leaves us a few options:

• Don't implement REPL in idris-lsp. Editor plugins could spawn a REPL in a terminal. This would require two Idris processes.
• Implement REPL in a completely custom way in idris2-lsp. This would require custom code for each editor.
• Use CodeLens like Haskell Language Server.
  • This requires explicit click to run
• Use something like #eval in Lean
  • Would be %eval in Idris
  • This runs automatically
  • Display result in info diagnostics? inlay hints? inline values? something else?
• For :exec, a code lens to click to run in a terminal
• Use Jupyter.
  • LSP may add support for notebooks.
• Use Debug Adapter Protocol.
  • DAP is not very popular and not that suited to Idris's needs.

Questions:

• Are there any better ways to tackles the issue than what I mentioned above?
• Would REPL state be cleared when changing focus between files?
• Would each file have its own REPL state?
• Would every file change reset the REPL?

[Russoul]

We can stick to native Idris2’ REPL behavior for your last three bullet points, at least provisionally.

That is:

• Keep state when changing between files. (There is no corresponding operation in the native REPL, but I don’t see why we’d want to wipe out the state on a file swap)
• Have one global REPL state.
• Every file change resets REPL.

[michaelmesser]

I'm not sure that it is possible to easily implement a :load that keeps the old state. I'm also not sure that every file change resetting the REPL is optimal (especially if/when the Idris API supports check as you type) because some users may want the REPL to stay on the last version with no errors.

[Russoul]

Wow, I actually completely missed that we have :load in idris2' REPL. Is it of any use for LSP users? Loading a file is as simple as opening it in the editor. Why would anyone want to do that via a command?

Holding off on resetting the REPL state until we've made sure the file type checked successfully sounds great. Keep the old state if the recent type-checking attempt resulted in errors.

[michaelmesser]

Another problem is that LSP doesn't have share Idris's concept of a single file loaded at a time. More than one file can be open at a time. In fact, we don't even know which document is currently focused, but we could have editor plugins tell us when focus changes or include the focused document when sending REPL commands. If there is a global REPL, instead of one REPL per file, how would the user specify which file would be loaded when the command is run?

[Russoul]

ATM, I personally think that if someone is interested in developing the idea into a working prototype, it's best to just stick to what's within easy reach based on what's currently offered by the Idris2 api. We've seen that api needs some reconstruction to accommodate all our wishes :) But that's a very long-term venture.

[michaelmesser]

The issue for Haskell Language Server is haskell/haskell-language-server#477. If they are able to find a solution, we may be able to do something similar.

[herkhinah]

LSP 3.17 has now support for notebooks.