EDIT: I installed coq-lsp
, and I'm running into a few issues. I see enough that I'm just collecting them into this thread.
Missing serlib plugin: coq-elpi.elpi
— is this warning a problem? _CoqProject
(even if it loads okay) nor if I rely on a pure dune
setup (aka, after rm _CoqProject
).Restart
and got Restart cannot be used through the Load command
, which is a first in my life since this code is Load
-free..._CoqProject
are ignored entirely, which makes my code very noisyissue 2. blocks me from trying this on most code from my work projects. All I _wanted_, tho, was to try this on _slow_ proofs to see how the interaction mode behaves, so I moved to my hobby project
Generally, this is pretty interesting!
Thanks a lot for testing @Paolo Giarrusso Indeed what @Ali Caglayan says, let me add a couple of extra points:
dune
filescoq/workspace.ml:parse_args
, that's an easy todo I thinkWhat do you need to enable / disable per-project? I'm not sure I understood
Regarding large proofs, IMHO we need some further improvements in Coq to handle them in the way I would like.
As of today, due to the way Coq works, it is not possible to "read" information of a document from, let's say, a different thread without interrupting what Coq is computing. That's a really bad point for systems like coq-lsp as when the user requests info you either:
First problem can be alleviated by using a cache, however there are non trivial tradeoffs involved. Let's see how things go.
Moreover there is no connection between the incrementality of the proof / logic programming engine and the incrementality at the sentence level, this is for sure desired in many scenarios.
What do you need to enable / disable per-project? I'm not sure I understood
s/project/workspace/g
— but Ali answered that: Vscode lets one disable extensions for workspace
Ah, you mean the extension itself: yes, it can be disabled per-workspace.
Happy to implement some other technique if folks have the need to tell coq-lsp "don't touch this"
Last updated: Mar 29 2024 at 15:02 UTC