IntellISense for Language Embeddings?

Stream: lean4

[Mac]

So I just finished a big update to Alloy that allows for the full embedding of C code into Lean and I am wondering how feasible would it be in either the short or long term to get the Lean extension to do C Intellisense on the C code -- or, more generally, augment the editor's IntelliSense in various ways from within Lean?

I imagine this would be a lot of work, but I know that it is possible for one language drive another in VS Code, I am curious if there is even the possibility of supporting this in the future and I would be more than happy to help where I can should such a project materialize.

[Gabriel Ebner]

See https://github.com/microsoft/language-server-protocol/issues/1366

[Gabriel Ebner]

augment the [completion LSP response] in various ways from within Lean?

I think that would be useful, also for other projects. I guess you could then start ccls as a subprocess, send it the current function as a C file, and then proxy the LSP requests.

[Mac]

@Gabriel Ebner Thanks! Yeah, I know that it is possible to interleave languages within a VS Code extension, but is it feasible for this (and/or other IntelliSense features) to be driven by Lean itself? Or would that likely need another VS Code extension on top of Lean 4 one to make such a thing possible? That is, would it be possible to do something like Widgets for IntelliSense (or can Widgets already do that)?

[Sebastian Ullrich]

It is not currently possible to override LSP request handlers from a Lean plugin, but that would be a trivial extension https://github.com/leanprover/lean4/blob/552a488f352a51e194cf9b5ddda908faf952e3b3/src/Lean/Server/Requests.lean#L142-L143

[Gabriel Ebner]

We don't really want to override here, we want to aggregate the results.

[Sebastian Ullrich]

Well, you can call the original one from the override :) . But a more general chaining system would be nice.

[Gabriel Ebner]

but is it feasible for this [...] features to be driven by Lean itself?

I think that's the most reasonable option. The LSP issue I've linked above says that that's their preferred approach. The vscode docs second this.

[Gabriel Ebner]

More concretely, I would just start a C language server (like ccls) from inside lean and use that to answer the completion requests.

[Mac]

@Gabriel Ebner Cool! I sadly have very little understanding of how the Lean server works, so I guess I had better start familiarizing myself with it. :laughing: Any tips, tricks, hints, advice on the Lean LSP that might help me orient such a project?

To illustrate my minimal knowledge on topic, my understanding (from what I have picked up in discussions) s that the elaborator builds up something called an 'info tree' which is used to handle requests. Thus, I imagine to do delegation here, the plugin would need to start a C language server, send/update the relevant C snippets to the server, keep some mapping between the C code locations and the Lean code locations in the info tree and then use those mapping to translate requests from client on the Lean the source to requests on the the C source which are then sent to the server. Is that somewhat right?

[Gabriel Ebner]

Yes, I think that's the right general approach. The part that isn't supported yet is hijacking the completion request for the Lean LSP server. But you can already experiment with starting the other LSP server, we have a pretty full-featured LSP library after all.

[Gabriel Ebner]

keep some mapping between the C code locations and the Lean code locations in the info tree

As far as I understand the alloy library doesn't do any fancy translation, it just prints the atoms and identifiers in the syntax tree to a C file. I would just compute this mapping in the completion request. You can get the macro-expanded syntax tree from the info tree, and you have the cursor position from the request, this should be enough information to craft a request to the C server.

[Mac]

@Gabriel Ebner wouldn't that still require reconstructing the entire C file worth of C commands on each request in order to determine where the offset from the current command's syntax is relative to the whole the C file? I guess, though, assuming that the reprint of the syntax tree to the C language server does not change any offsets within the command, that would just some basic addition of the lengths of each command's syntax.

[Gabriel Ebner]

Yes, but I don't think the position computation is a big problem. ∑ previous_commands + index_in_current_one (I'm not sure if the C server needs some time to process the file.)

[Mac]

@Gabriel Ebner Makes sense. One other question: is it feasible to leverage the existing C language server used by the user's VS Code extensions to handle the request, rather than choosing one server and starting that? The reason I ask, is that I imagine if Lean starts it own server it may not be configured in the same way as the one the user usually uses in VS Code (or whatever LSP client is being used).

[Gabriel Ebner]

is it feasible to leverage the existing C language server used by the user's VS Code extensions to handle the request, rather than choosing one server and starting that?

Which LSP server to start, and what arguments (include paths) to give it is a valid issue. Note that users may also use other editors than vscode. I'm not aware of any general way to get the LSP binary path + arguments for another extension from within vscode.

[Julian Berman]

Is https://code.visualstudio.com/api/language-extensions/embedded-languages#language-services a thing to read?

[Julian Berman]

It seems to be what https://github.com/microsoft/vscode-html-languageservice uses which surely has to deal with similar things

[Gabriel Ebner]

AFAIU, language services are just LSP-servers-as-a-library.

[Julian Berman]

It doesn't seem they're too different from my skim so far, yeah -- there's some sample code it seems here https://github.com/microsoft/vscode-extension-samples/tree/main/lsp-embedded-language-service that I'm about to flip through

[Mac]

Gabriel Ebner said:

Note that users may also use other editors than vscode. I'm not aware of any general way to get the LSP binary path + arguments for another extension from within vscode.

There is Request Forwarding on the client side to invoke another language extension to handle requests. I'm not sure if there is a way to do this server side, though.

[Mac]

I am resuscitating this old thread because I have developed Alloy to the point where the last major feature it needs is C/C++ LSP support. I have installed ccls as a test language server to call out to and plan to use the chainLspRequestHandler (from the old PR) to pass requests along to it. However, I am not very well versed on the inner workings of an LSP. Does anyone have any advice on how to proceed from here and/or tips on what I should watch out for in this undertaking?

[Mac]

Also, IIRC and understand the code, request handlers can only be registered via plugins (through builtin_initialize), not by normal initialize blocks. I am curious as to what the rational behind that is?

[Mac]

One major problem I am having is the C/C++ language servers (clangd and ccls) both seem to want to have a real directory and real files to compile. That is, while the LSP specification supports virtual documents, clangd and ccls do not appear to.

[Mac]

Okay, so apparently providing it with a blank c file and then the virtual document does work (it uses the text of the virtual document), but just the virtual document without a corresponding c file does not?

[Mac]

Hilariously, this means that passing file:///dev/null as the document uri works to create a virtual document, but I don't think there is a parallel on non-MSYS2 Windows?

[Sebastian Ullrich]

Windows has some "fun" pseudo files in any folder https://stackoverflow.com/questions/313111/is-there-a-dev-null-on-windows

[Mac]

Thanks! Yep, just saw that.

[Mac]

Does Lean have any synchronization primitives (e.g., locks / mutexes)? I am not sure how else I am suppose to synchronize message and version ids across the various request threads (plus other shared state about the connection with the language server).

[Sebastian Ullrich]

https://github.com/leanprover/lean4/issues/1280

[Sebastian Ullrich]

IO.Ref works well enough for the Lean language server

[Mac]

Thanks again! I should probably be looking for these things before I ask the question. :laughter_tears:
(It is also morning and I have yet to sleep so that may be part of the problem. :zzz:)

[Mac]

I guess my last major question for the moment (which there may also already be an easy answer I have not yet found): is there a way to hook into the Lean server's main loop to forward request / diagnostics from C server or should I just invoke publishDiagnostics etc. directly from the request handlers I am chaining?

[Sebastian Ullrich]

If you don't somehow change the behavior of the current publishDiagnostics-calling code, the two different sets of messages will just override each other in the editor, no?

[Mac]

So I have made a lot of progress on Alloy with LSP integration and have got basic hovers working (still need to have a proper work thread for the server, though). However, I encountered this fun bit of formatting when it comes to markdown hover text:

AlloyMarkdownHoverFormatting.PNG

Is there some way to get this to render nicer @Gabriel Ebner , @Wojciech Nawrocki , or @Chris Lovett? I made sure to update to the VSCode Lean 4 extension to v0.0.84 because I thought that the line height may have been fixed by Wojciech's PR #215, but unfortunately it was not.

[Gabriel Ebner]

The hovers are completely different from the infoview issue.

[Gabriel Ebner]

Can you post the markdown that you're sending?

[Mac]

clangd produces the following markdown for the hover above:

### function `printf`

---
→ `int`
Parameters:
- `const char * __format`

---
```objective-cpp
inline int printf(const char *__format, ...)
```

[Gabriel Ebner]

Okay, then it renders just as it should.

[Mac]

@Gabriel Ebner the horizontal line is suppose to merge with the code block that comes after it?

[Gabriel Ebner]

Ah, now I see what you mean. I was distracted by the headline followed by a horizontal line followed by an arrow.

[Gabriel Ebner]

I'm using ccls instead of clangd, which has more sensible hovers. (Docstring followed by horizontal line followed by type signature.)

[Mac]

I am using clangd because I was having great difficulty getting ccls to work in a root-less, virtual document manner.

[Mac]

ccls wants file:// document URIs and does not seem to allow the file:///dev/null/ trick I figured out to get clangd to work with virtual documents.

[Mac]

While the null URI tricks does allow the ccls server to run, it will complain that the virtual document is not indexed and error out.

[Mac]

@Gabriel Ebner so is the verdict that there is no neat way to fix the formatting? I put an extra newline between the bar and the the code block (thinking that the grouping maybe be the problem) but that still did not work:

### function `printf`

---

→ `int`
Parameters:
- `const char * __format`

---

```objective-cpp
inline int printf(const char *__format, ...)
```

[Gabriel Ebner]

The formatting works "as intended". clangd wants weird horizontal bars and duplicate type signatures, so it gets them. Just to make sure, do you get the same formatting if you use clangd directly on a C file?

[Mauricio Collares]

The problem is the non-existent padding between the second horizontal line and the code block, I assume?

[Gabriel Ebner]

Personally, I think the whole message is the problem. But I believe Mac is particularly unhappy about the missing padding, yes.

[Gabriel Ebner]

https://github.com/clangd/clangd/issues/747

[Mac]

Another question, @Gabriel Ebner / @Wojciech Nawrocki : Is there anything wrong with lightening the requirement of register/chainLspRequestHandler from builtin_intiialize to just initialize (so that users can register/chain handlers without plugins)? I am currently doing that manually by copying the definition and removing the check, but it seems feasible to do it in core as well (though we probably do want at least an Lean.initializing check there).

[Wojciech Nawrocki]

I can never remember why that check is there, so it's probably fine?

[Mac]

On a somewhat related note, I ended up encoding the entirety of the ClientCapabilities LSP specification into Lean for Alloy (see here). Is that something worth PR'ing @Wojciech Nawrocki? (I'm asking you as you are one of the authors of the current fragment of the specification in the Lean core).

[Wojciech Nawrocki]

Hm, are you planning to make use of having these in core? I think the attitude so far has been to add what we need but ignore the rest.

[Mac]

True. No, I don't have any plans at the moment. My reason for asking was that some of the TODOs in the server code (such as here and here) suggested to me that the goal of the LSP code may be to encode the entire LSP specification, but what was done thus far was just what was most expedient to complete (and necessary for the Lean server's current functionality). Thus, I was curious if a PR of some of the rest of the specification would be appreciated.

[Sebastian Ullrich]

@Mac Since you've already done the work, I think it would be a waste not to upstream it. Especially since maintenance and, hopefully, compilation overhead should be pretty low.

[Gabriel Ebner]

I've sometimes wondered if we shouldn't store the original json for open-ended definitions like the client capabilities. Any fixed schema is going to truncate something here. In particular it is impossible to access any of the left out fields from user code, because the watchdog already strips it out.

structure WithOriginalJson (α : Type u) where
  val : α
  json : Json

instance : FromJson (WithOriginalJson α) where
  fromJson? j := return ⟨← fromJson? j, j⟩

instance : ToJson (WithOriginalJson α) where
  toJson := WithOriginalJson.json

[Wojciech Nawrocki]

Hm, are you planning to make use of having these in core? I think the attitude so far has been to add what we need but ignore the rest.

[Mac]

Gabriel Ebner said:

I've sometimes wondered if we shouldn't store the original json for open-ended definitions like the client capabilities. Any fixed schema is going to truncate something here.

While I do I like idea, it is worth noting that client capabilities are not an open-ended definition according to the schema. There is one field experimental which is user defined (and which I implement by parameterizing ClientCapabilities by a type Experimental which defaults to Json), everything else is very fixed (according to the spec -- that of course doesn't stop implementers from violating the spec).

[Gabriel Ebner]

This is a good point. I was actually thinking of upgrades in the LSP specification version. Because that's precisely where you need client capabilities: to figure out if the client supports the newest feature that just appeared in the spec today. But I guess that's similar to new fields being added to Diagnostic.

[Mac]

New problem: the Lean LSP specification does not support the full range of default semantic tokens and modifiers, thus I can't forward the highlights for such tokens from clangd. Would a quick PR that expands SemanticTokenType and SemanticTokenModifier to include the full list be welcomed?

[Mac]

I went ahead and made one: #1325. Hope that is okay. (Still need to wait to make sure I didn't break anything, though.)