Stream: coq-lsp

Topic: General Chat


view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:10):

Hi @Ali Caglayan let's use this for general chat

view this post on Zulip Ali Caglayan (Oct 06 2022 at 16:10):

OK so you mentioned that the viewport needs work in editor/code and also some elisp script for emacs right?

view this post on Zulip Ali Caglayan (Oct 06 2022 at 16:11):

coqlsp should handle a query which asks for the goals panel at a point right?

view this post on Zulip Ali Caglayan (Oct 06 2022 at 16:11):

and the clients can use that for their panels

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:16):

We said a few interesting things to do, I'll summarize:

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:16):

Ali Caglayan said:

coqlsp should handle a query which asks for the goals panel at a point right?

Yup, see the code in lambdapi

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:16):

what we have done in jsCoq is we just bind click or M-Enter to send goals

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:16):

then when the notificaiton arrives we just display them

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:17):

I will code that PR next porting the lambdapi code, so I suggest you wait for the skeleton to be in place, then we tweak

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:19):

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:20):

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:22):

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:22):

that's fun too

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:35):

Another one: a test suite :devil:

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:35):

:smiling_devil:

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:35):

:satellite_antenna:

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 16:36):

and of course, coordiantion work which as you can see it is pretty challenging, tho I'm putting a lot of effort on my slides for Fri so that should be a base

view this post on Zulip Emilio Jesús Gallego Arias (Dec 19 2022 at 15:14):

@Ramkumar Ramachandra are you working on the progress bar issue? If not, I'll give it a go this afternoon

view this post on Zulip Ramkumar Ramachandra (Dec 19 2022 at 16:21):

@Emilio Jesús Gallego Arias No, I'm not working on it.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 19 2022 at 16:34):

Ok, taking the lock on that

view this post on Zulip Emilio Jesús Gallego Arias (Dec 24 2022 at 02:26):

A prototype that seems to work pretty well has been submitted; still I need to fix the mapping to the editor, but seems ready otherwise.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 02 2023 at 22:41):

Hi folks, still not fully back from holidays, but I'll try to do a pass on the github pending list

view this post on Zulip Emilio Jesús Gallego Arias (Jan 02 2023 at 22:41):

anything urgent?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 02 2023 at 22:54):

Thanks for all the work folks while I was away.

Note that we should spend some time implementing a small test suite, the LSP reference implementations / example already have one. That becomes a must as development picks up speed. We can do something basic like:

view this post on Zulip Ali Caglayan (Jan 03 2023 at 11:40):

I will have a think about how we might go about that. We probably won't need to pull in anything particularly heavy handed like the LSP extension test suites I have seen around.

view this post on Zulip Ali Caglayan (Jan 03 2023 at 11:40):

Something similar to the fakeide tests we have in Coq should be ideal.

view this post on Zulip Ali Caglayan (Jan 03 2023 at 11:41):

Of course, those are a PITA to write, so I will try to make it simple to set up.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 03 2023 at 14:42):

I didn't find the testing setup in the LSP examples particularly heavy-handed

view this post on Zulip Emilio Jesús Gallego Arias (Jan 03 2023 at 14:42):

which suites you saw around?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 08 2023 at 18:46):

Hi @Huỳnh Trần Khanh , you recently mentioned that it seems that coq-lsp feels pretty barebone, have you tried 0.1.2?

What are the most important features do you think that 0.2.0 should ship?

view this post on Zulip Karl Palmskog (Jan 08 2023 at 19:05):

saw the announcement. I think it would be a good idea to emphasize this is only compatible with 8.16+ (for which there is no regular Coq Platform release yet and no Snap, for example)

view this post on Zulip Emilio Jesús Gallego Arias (Jan 08 2023 at 19:26):

Yes, it'd be good to precise this. Tho it people is interested, we can add support quite a few releases back.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 08 2023 at 19:27):

In fact coq-lsp is really 8.17 only, but we hacked 8.16 support to release in OPAM. We will add a (yet unnamed) "coq-extra-patches" to opam which for each release will be 8.17 plus patches for coq-lsp adding some needed features.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 08 2023 at 19:28):

But in general compat for this stuff is like in Isabelle, coupled to a particular release, specially if we want to ship some of the nicer features

view this post on Zulip Emilio Jesús Gallego Arias (Jan 08 2023 at 19:28):

I didn't have the time but I'd like to add a coq-lsp package for coq-opam-archive and 8.17

view this post on Zulip Emilio Jesús Gallego Arias (Jan 08 2023 at 19:37):

Very happy to take pull requests or edits in the discourse post, or replies to Coq club.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 08 2023 at 19:39):

Ok, replied to myself in Coq Club

view this post on Zulip Huỳnh Trần Khanh (Jan 10 2023 at 15:35):

Emilio Jesús Gallego Arias said:

Hi Huỳnh Trần Khanh , you recently mentioned that it seems that coq-lsp feels pretty barebone, have you tried 0.1.2?

What are the most important features do you think that 0.2.0 should ship?

Haven't tried 0.1.2 yet. I even thought that the coq-lsp extension was _intentionally_ bare bones! I mentioned in the last meeting that we directly interpolate strings into HTML. And yeah, you did say that the attack surface is small, and I do agree. But we web developers only do this kind of string concatenation when we make a quick demo, and by this logic, I thought the extension was also... a quick demo too, and there would be another more "serious" extension that uses coq-lsp behind the scenes. I guess we could rewrite the infoview code in a similar way as what I've done in the VsCoq repo. A nice benefit is it would be easier to add fancy features like the Lean infoview. BTW in the meeting I saw that you were using Lean 3, but the Lean 4 extension is where it's at!

view this post on Zulip Huỳnh Trần Khanh (Jan 10 2023 at 15:38):

I'm also looking forward to lending you a hand. I don't know OCaml yet but it looks similar to Coq so I think I can learn that easily, and I also have a nice textbook that teaches some basics.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2023 at 19:24):

Hi @Huỳnh Trần Khanh , thanks for your thoughts!

Indeed a design goal of coq-lsp is to be quite lightweight, in particular to be sure that API layering with Coq is seamless, otherwise things become hard to maintain.

I can understand the confusion about extensions, I'm very confused too honestly, I will post one the vscoq thread to state what I know.

Yes, thanks for the Lean 4 reference, indeed I also have lean 4 installed, and I'm familiar with it.

Working on the infoview could be great, do you have a pointer to what you did / things you would like to see happen there?

Regarding the injection indeed the security model should be enough, but for sure that part is a prototype, we will replace that soon with the jsCoq printer)

view this post on Zulip Ori Lahav (Feb 05 2023 at 18:50):

Hi,
I get the error:

[Error - 8:47:33 PM] Stopping server failed
Message: Pending response rejected since connection got disposed
Code: -32097

Anything I'm doing wrong? It worked earlier. Any way to reset?

view this post on Zulip Ali Caglayan (Feb 05 2023 at 19:03):

If you do Ctrl + P and press >coq you should see something about restarting LSP. Try that.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 05 2023 at 20:39):

Hi @Ori Lahav , seems the server stopped working, what do you see in Output > Coq LSP Server Events ?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 05 2023 at 21:00):

Better if you can go to settings and enable Coq-lsp > Trace: Server

view this post on Zulip Ori Lahav (Feb 06 2023 at 05:00):

Here is the output
coqlsp.txt
Thanks!


Last updated: Feb 06 2023 at 05:03 UTC