Hi @Ali Caglayan let's use this for general chat
OK so you mentioned that the viewport needs work in editor/code and also some elisp script for emacs right?
coqlsp should handle a query which asks for the goals panel at a point right?
and the clients can use that for their panels
We said a few interesting things to do, I'll summarize:
didChange
supports progress eventsAli Caglayan said:
coqlsp should handle a query which asks for the goals panel at a point right?
Yup, see the code in lambdapi
what we have done in jsCoq is we just bind click or M-Enter to send goals
then when the notificaiton arrives we just display them
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
that's fun too
Another one: a test suite :devil:
:smiling_devil:
:satellite_antenna:
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
@Ramkumar Ramachandra are you working on the progress bar issue? If not, I'll give it a go this afternoon
@Emilio Jesús Gallego Arias No, I'm not working on it.
Ok, taking the lock on that
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.
Hi folks, still not fully back from holidays, but I'll try to do a pass on the github pending list
anything urgent?
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:
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.
Something similar to the fakeide tests we have in Coq should be ideal.
Of course, those are a PITA to write, so I will try to make it simple to set up.
I didn't find the testing setup in the LSP examples particularly heavy-handed
which suites you saw around?
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?
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)
Yes, it'd be good to precise this. Tho it people is interested, we can add support quite a few releases back.
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.
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
I didn't have the time but I'd like to add a coq-lsp package for coq-opam-archive and 8.17
Very happy to take pull requests or edits in the discourse post, or replies to Coq club.
Ok, replied to myself in Coq Club
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!
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.
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)
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?
If you do Ctrl + P
and press >coq
you should see something about restarting LSP. Try that.
Hi @Ori Lahav , seems the server stopped working, what do you see in Output > Coq LSP Server Events ?
Better if you can go to settings and enable Coq-lsp > Trace: Server
Here is the output
coqlsp.txt
Thanks!
Last updated: Mar 29 2024 at 10:01 UTC