RedPRL
🖥️ Add example configurations for LSP servers
It would be a good idea to add some example configurations for various editors, so we could just copy+paste when using asai.lsp in other projects.
Unfortunately, the situation with lsp-mode is pretty grim; see https://github.com/emacs-lsp/lsp-mode/issues/3625
Perhaps we (or I?) should spend a bit more time resolving this issue. 😅 @TOTBWF What's the current progress of fixing bugs in the cited issue?
@mikeshulman Is there a particular editor you want to try out first?
I discussed the issue with the maintainers and it's a WONTFIX 😔 However, it looks like the emacs community has decided that https://github.com/joaotavora/eglot is the implementation of choice, and has upstreamed it into emacs proper.
It appears that they have an opt-in mode that does the right thing with UTF-16; not sure if UTF-8 is supported, or if they've implemented the position encoding handshake from LSP 3.17. I'll try and ask on IRC
@TOTBWF I see, but no, I don't think that's the main issue or difficulty here. There's no need to try to work around UTF-8/16 now---at least that's not the priority. The main issue here is the documentation. In @mikeshulman's case, I strongly suspect that the prototype only uses ASCII, so none of the encoding issues should matter.
I don't use emojis, but I'm a big fan of unicode math symbols. In fact one of the reasons I picked fmlib_parse was that it seemed like the best lexer/parser combination for dealing with utf8. So no, I'm not using only ASCII.
I am also a dedicated Emacs user, but not particularly a fan of things that try to compile/typecheck my code while I'm writing it.
not particularly a fan of things that try to compile/typecheck my code while I'm writing it.
Maybe that's an exaggeration. I don't hugely mind the way tuareg highlights errors in my OCaml code in real-time, although I like that it doesn't do it until I save the file. In fact I would prefer to have a separate command to make it do that, so that if I'm making a big breaking change I can save while I'm partway through it even though what's currently in the file is not syntactically correct without causing huge amounts of the code to be highlighted. (Maybe there's a configuration option for that, I haven't found it but I haven't looked really hard.)
But I've had pretty unpleasant experiences with Lean. A lot of that is probably due to the typechecking not always being instantaneous (unlike with OCaml), so it's hard to tell whether the automatic highlighting is in sync with the text or not.
I'm not sure this is relevant at all to what we're talking about here though.
@mikeshulman The speed is indeed important, especially for auto-completion. So we were thinking about promoting the design of having a separate scope-checker to give quick feedback on whether there's a typo, etc. None of these ideas have been realized so I can't really make any useful comment. 😅