Stream: coq-lsp

Topic: Adding string repr to the `Goal` object

Bhakti Shah (Mar 26 2023 at 03:11):

Does it make sense to add a field with just the string representation of the hypotheses and goals to the Goal Object returned by the proof/goals request? If I'm looking at it right, the information returned isn't very human readable, and I'm working on something where just the literal string representation of the goal would be useful. Thanks!

Gaëtan Gilbert (Mar 26 2023 at 11:29):

It is not meant to be human readable
You can try to use Printer.Debug.pr_goal on it I guess

Emilio Jesús Gallego Arias (Mar 27 2023 at 15:46):

@Bhakti Shah yes, I think it would make sense, actually if you look at the current type definition , https://github.com/ejgallego/coq-lsp/blob/936f73a992be2a10445304f35beec572963f9923/editor/code/lib/types.ts#L18

it is already parameterized by the return type Pp.

So we can extend that to be like in SerAPI, and include a format type for users.

As of today note we can return either strings or that type you see now CoqPp, which is actually not so complex.

Let me review your PR and I can provide more feedback.

Bhakti Shah (Mar 28 2023 at 19:05):

Yeah so I experimented a bit and when I set pp_type to 0 in package.json (so just the string), i get the information exactly as I want it. obviously i dont want to make such a big change given that the jscoq formatting is so much nicer, but I don't see a way of sending a request to the server with a specific type I want my output in -- if I could send a standalone request that returned the object in the string representation that would be perfect, but as far as i can tell the requests arent parameterized by this and pp_type is just declared in package.json and globally constant. Is this actually true? I might just be missing something here.

I see two solutions to my issue -- if there is in fact a way to make a request with a specific output type, that would be pretty simple for me to add. if there isn't, and making this actually variable seems like a big task, I can also just see a field being added to the jscoq object type that just has the string representation.

I'm more than happy to work with either of these solutions, and happy to make a PR for the same, but I would just want to know if you have a preference regarding the same. Particularly if making the pp_type variable in a single instance is something you plan on doing anyway in the future, it would be great to know. Thank you!

Emilio Jesús Gallego Arias (Mar 29 2023 at 14:06):

Hi @Bhakti Shah , sorry I'm not very responsive, pretty busy this week.

I think the best way would be to add the type of object your extension needs to a registration API, so indeed, you would register a callback requiring the goals to have a string carrier, and coq-lsp will provide you a goals object with the right type.

Adding an extra field scales poorly as in general we have N output formats.

So what I propose is:

• generalize the proof/goals request type as to include the desired output type (like done in SerAPI)
• adding a registerGoalProccesor API that would take the method with the right goals type
• coq-lsp will issue the queries in the format the registered extensions need

How does that plan sound to you?

I think indeed that for your use case, string will become quickly too weak, and indeed you may want a higher-level representation of what's on the goal, like the one provided by the layout-printer, so going this way would allow you to experiment better with alternatives

Emilio Jesús Gallego Arias (Mar 29 2023 at 15:18):

First item done in https://github.com/ejgallego/coq-lsp/pull/470

Bhakti Shah (Mar 29 2023 at 23:00):

That's great, thank you! Yes, adding the API sounds good -- I think that was the best possible result but it seemed like a much bigger change. I can work on making a PR for that if you aren't working on it already. Let me know if there are other things you would want to add to the API too, although I suspect it'll either be bare bones suited to user needs or a full fledged API depending on what you want.
For now I'll use the parameter for the proof/goals request and possibly make an updated PR once I've tested that it is what I want.

Emilio Jesús Gallego Arias (Mar 29 2023 at 23:02):

Great! I suggest you do whatever you need to make things working smoothly for you

Emilio Jesús Gallego Arias (Mar 29 2023 at 23:03):

For now we can just make the request twice, it will be cached server-side

Emilio Jesús Gallego Arias (Mar 29 2023 at 23:03):

and we dispatch the right result type to the right place

Emilio Jesús Gallego Arias (Mar 29 2023 at 23:15):

I think it'd be great if you make a PR so that you can register your plugin for the action that you need

Emilio Jesús Gallego Arias (Mar 29 2023 at 23:16):

At some point if you have a test suite let me know so I can test your plugin in the CI to ensure that it is not broken

Bhakti Shah (Mar 29 2023 at 23:27):

Hm okay so I'm playing around with it and it seems I should just be sending a request with the pp_format specified -- and this is what I'm using:
let strCursor: GoalRequest = {textDocument, position, pp_format: "Str"};
and I'm basically using the same pipeline as the requestDisplay but you can see the code here if you'd like

I'm still getting the same goals object in response, not the one I was seeing when I set the pp_format parameter globally. I'm guessing this isn't the desired behavior?

Emilio Jesús Gallego Arias (Mar 29 2023 at 23:40):

Indeed it seems like a bug

Emilio Jesús Gallego Arias (Mar 29 2023 at 23:40):

Let me re-test (I should have added a test to my PR)

Emilio Jesús Gallego Arias (Mar 29 2023 at 23:42):

Works fine here @Bhakti Shah , maybe check you did recompile the binary ?

Bhakti Shah (Mar 30 2023 at 00:38):

I did recompile, but i wonder if having lsp installed globally is an issue? like maybe it's using the globally installed version

Bhakti Shah (Mar 30 2023 at 00:40):

Yeah, I'm not sure how to make it look at the new binary and not the globally installed one? I did the dune exec and everything but it always seems to use the global install.

Bhakti Shah (Mar 30 2023 at 00:55):

I believe dune exec is not actually updating my env variables as when there is no global install, the server does not run. I'll manually make the changes and see if that works

Ali Caglayan (Mar 30 2023 at 01:03):

When you do dune exec the env vars will only be available to whatever you are running

Ali Caglayan (Mar 30 2023 at 01:03):

Are you running an editor or something?

Ali Caglayan (Mar 30 2023 at 01:03):

For example, for vscode I do dune exec -- code ..

Ali Caglayan (Mar 30 2023 at 01:04):

That gives the correct PATH with coq-lsp in it

Bhakti Shah (Mar 30 2023 at 01:04):

yeah i just ran dune exec --code editor/code

Ali Caglayan (Mar 30 2023 at 01:05):

Try dune exec --root=editor/code -- code . isntead

Ali Caglayan (Mar 30 2023 at 01:06):

or nevermind that won't work

Ali Caglayan (Mar 30 2023 at 01:06):

If you do dune exec -- echo $PATH you should see _build/install appear

Bhakti Shah (Mar 30 2023 at 01:07):

hm yeah it does

Ali Caglayan (Mar 30 2023 at 01:07):

And make sure you have actually built coq-lsp with dune build @install.

Ali Caglayan (Mar 30 2023 at 01:08):

Since dune execis not running anything that Dune knows the deps of it won't force a build of coq-lsp

Bhakti Shah (Mar 30 2023 at 01:11):

yeah I have

the coq file i'm testing is not in the editor/code directory (so the one i open when i launch the extension) -- could that be an issue? when i echo $PATH in the extension development host window it doesn't show me _build/install

Ali Caglayan (Mar 30 2023 at 01:19):

yes thats probably the issue

Ali Caglayan (Mar 30 2023 at 01:20):

I usually symlink editor/code to my extesnions folder

Ali Caglayan (Mar 30 2023 at 01:20):

that way when I start vscode in dune exec -- code . at the root of the repo, vscode finds the extension through the symlink

Ali Caglayan (Mar 30 2023 at 01:21):

There is a detailed guide how to do this in https://github.com/ejgallego/coq-lsp/blob/main/CONTRIBUTING.md

Ali Caglayan (Mar 30 2023 at 01:22):

If you don't need the latest extension (typically you dont) then just install the extension from the vscode store

Ali Caglayan (Mar 30 2023 at 01:22):

look up coq-lsp you will find it

Ali Caglayan (Mar 30 2023 at 01:22):

Then when you dune exec -- code . it will have the correct coq-lsp in path

Bhakti Shah (Mar 30 2023 at 01:27):

So I've been following exactly what's in the contributing guide

and i do think I need the latest extension because i need the changes just pushed to the server to test my client side code

Bhakti Shah (Mar 30 2023 at 01:28):

let me try symlinking

Bhakti Shah (Mar 30 2023 at 01:29):

though i don't think the extension is the problem - it's the server that the extension cannot find

Bhakti Shah (Mar 30 2023 at 01:38):

yeah symlinking didn't do anything

Ali Caglayan (Mar 30 2023 at 01:43):

The issue with vscode is that when you start a debug session or whatever it is called, it doesn't inherit the env

Ali Caglayan (Mar 30 2023 at 01:44):

That would be my guess to what is going on

Bhakti Shah (Mar 30 2023 at 01:45):

yeah that is what i am thinking because the path isnt updating in the development server -- but i'm wondering how anyone is able to test server side code within the extension then

Ali Caglayan (Mar 30 2023 at 01:45):

I just run dune exec -- code editor/code like you said

Ali Caglayan (Mar 30 2023 at 01:45):

ah you did symlink

Ali Caglayan (Mar 30 2023 at 01:45):

but did you "build" the extension

Ali Caglayan (Mar 30 2023 at 01:46):

do make extension

Ali Caglayan (Mar 30 2023 at 01:47):

Then when you run do dune exec -- code . you should have the latest extension and coq-lsp (if you built it)

Bhakti Shah (Mar 30 2023 at 01:50):

yeah i tried it manually but no luck; and also the vscode debug session automatically builds it too

when i launch it it seems to be running the right version:

coq-lsp@0.1.7 watch
 npm run esbuild -- --watch


 coq-lsp@0.1.7 esbuild
 node esbuild.mjs "--watch"

because if im not wrong 0.1.7 is not released yet and has to be the version I have locally

Emilio Jesús Gallego Arias (Mar 30 2023 at 13:58):

Yes, 0.1.7 is not released yet

Emilio Jesús Gallego Arias (Mar 30 2023 at 13:58):

That's bizarre, looking forward to a better setup, especially that now we gotta test 2 extensions

Emilio Jesús Gallego Arias (Mar 30 2023 at 14:00):

What I always do on Linux, and so far with success is

1. dune exec -- code editor/code this sets the path right
2. press F5 to launch the extension
3. edit and makethe server
4. eventually reload the vscode instance, restart the lsp server, etc...

Emilio Jesús Gallego Arias (Mar 30 2023 at 14:00):

Setting path directly in options can be of help too

Bhakti Shah (Mar 30 2023 at 22:53):

Yeah so I tried manually adding all the env variables that i think were modified by dune exec, dont know if this is something that's listed more clearly somewhere but i don't think it worked :( will try possibly running on linux instead of mac?

Emilio Jesús Gallego Arias (Mar 30 2023 at 23:17):

Linux or mac shouldn't matter, most reliable is just add the path to coq-lsp in the config section.

Are you sure the problem is not elsewhere? It seems to me you may be running the good binary, what commit are you, what is your concrete test that fails?

Here, using this diff I can observe the difference on main:

diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts
index 1866e33..08e396e 100644
--- a/editor/code/src/goals.ts
+++ b/editor/code/src/goals.ts
@@ -99,6 +99,7 @@ export class InfoPanel {

   // LSP Protocol extension for Goals
   sendGoalsRequest(client: BaseLanguageClient, params: GoalRequest) {
+    params.pp_format = "Str";
     this.requestSent(params);
     client.sendRequest(infoReq, params).then(
       (goals) => this.requestDisplay(goals),

Bhakti Shah (Mar 30 2023 at 23:29):

So basically I've deleted my opam installed lsp binary as well as the extension. when i launch it using the development host, it just gives me the standard could not connect to server error:

[Error - 6:29:09 PM] Coq LSP Server client: couldn't create connection to server.
Launching server using command coq-lsp failed. Error: spawn coq-lsp ENOENT

Bhakti Shah (Mar 30 2023 at 23:30):

it's not an issue in the code, i just think my computer won't recognize the non opam lsp binary even after i set all the environment variables manually? which doesn't really make sense

Emilio Jesús Gallego Arias (Mar 31 2023 at 03:12):

What does _build/install/default/bin contain?

Emilio Jesús Gallego Arias (Mar 31 2023 at 03:13):

Also there is a thing about code

Emilio Jesús Gallego Arias (Mar 31 2023 at 03:13):

If you do dune exec -- code editor/code

Emilio Jesús Gallego Arias (Mar 31 2023 at 03:13):

You need code to be not open already I think

Emilio Jesús Gallego Arias (Mar 31 2023 at 03:13):

otherwise it will reuse the existing session elsewhere

Emilio Jesús Gallego Arias (Mar 31 2023 at 03:14):

and I think indeed PATH won't be altered

Emilio Jesús Gallego Arias (Mar 31 2023 at 03:14):

very likely this is your issue

Emilio Jesús Gallego Arias (Mar 31 2023 at 03:15):

You can check running echo PATH from the VS Code terminal

Paolo Giarrusso (Mar 31 2023 at 03:41):

Beware the vscode terminal might not show the vscode PATH: That starts a new shell, which will likely load ~/.bashrc or the like (but not ~/.profile or the like; shell init is complex)

Bhakti Shah (Mar 31 2023 at 03:46):

I see -- yeah, I was opening it while vscode was open, and you were right -- it works fine now ! i was checking the env from the vscode terminal and the information wasn't populated there so yeah that makes sense

thank you so much for the help!

Ali Caglayan (Mar 31 2023 at 20:15):

I think code -n forces the opening of a new session. I forgot about htis because I configured code to always do this unless a project is already open.

Last updated: Apr 20 2024 at 06:02 UTC