Comments (13)
An OCaml implementation of LSP data structures is here: https://github.com/facebook/hhvm/blob/master/hphp/hack/src/utils/lsp.ml
Would we get then a TODO list, it should be easy to support this in a basic sense. Some more advances capabilites of the LSP are quite hard to do due to Coq internals.
from coq-serapi.
This is well on the road and working now; it wouldn't be unreasonable to expect SerAPI to build on the LSP kernel for 0.7.0
from coq-serapi.
I'd like to help with this issue, do you know of some relatively self-contained work that needs to get done to support LSP?
from coq-serapi.
@LilRed as I mentioned in the other issue, there is an in-progress branch. If you can I can give you access, but we'd still like to rewrite the whole server implementation before releasing to better account for the nuances of inter-process communication.
from coq-serapi.
@ejgallego any chance I can get access to the in-progress branch?
from coq-serapi.
@LilRed I could give you access to the tree however that wouldn't help a lot; the main issue here and where work is concentrated now is in the base Coq API for incremental document checking.
Until that is ready, proper LSP is too hard to implement reliably IMO. So first we are working on icheck
, then coq-lsp
will be built on top of that [and serapi too].
I hope a first "alpha" version of icheck
is ready soon, so indeed at that point we could try to make the lsp code work; what are your goals? I'd be great indeed to setup the minimal amount of code so collaboration is possible.
As for now, the Coq branch of the LSP server is basically this code but adapted to Coq without significant changes.
from coq-serapi.
what are your goals?
Broadly, to invest in something Coq-related for ~150 hours with between February and April. Also, I'd like to do my part towards moving on from CoqIDE to something more flexible and modern. Not that CoqIDE is particularly bad, in fact it's surprisingly good, but it's not easily extensible and I haven't figured out how to "look under the hood" and work around its warts.
the main issue here and where work is concentrated now is in the base Coq API for incremental document checking
Can you point me to that work? Or is it not publicly accessible?
Best
from coq-serapi.
Hi @LilRed , indeed I think your timeframe should work pretty well.
Can you point me to that work? Or is it not publicly accessible?
Sure, I will give you some pointers in the next weeks; the reason the current prototype is not publicily accessible is that it is still not usable and I feel it would make many people lose a lot of time.
Indeed, the current prototype needs a full rewrite once we improve the Coq API itself, but that should happen pretty soon as we have made quite a bit of progress on the Coq side; the Coq PR allowing for the icheck / LSP prototype to function should land in master
soon.
from coq-serapi.
the Coq PR allowing for the icheck / LSP prototype to function should land in master soon.
What PR would that be? :)
from coq-serapi.
@LilRed for example coq/coq#10681 and coq/coq#10884 and a couple other more that have not been submitted yet.
See also coq/coq#10041
from coq-serapi.
Also, I'd like to do my part towards moving on from CoqIDE to something more flexible and modern. Not that CoqIDE is particularly bad, in fact it's surprisingly good, but it's not easily extensible and I haven't figured out how to "look under the hood" and work around its warts.
Note that VsCoq (https://github.com/coq-community/vscoq) is pursuing very similar goals.
from coq-serapi.
@LilRed for example coq/coq#10681 and coq/coq#10884 and a couple other more that have not been submitted yet.
Welp, that's indeed on the Coq side, and rather deeper stuff than I can chew as of right now. If that's where the action is I'm going to start digging into Coq internals as soon as I have time. If you know of any particularly useful introductory material or well-defined low-hanging fruit that a newcomer could likely deal with, let me know.
from coq-serapi.
Thanks @LilRed , I'm unsure if there is any resource that would help right now; hopefully the situation does improve before Christmas.
from coq-serapi.
Related Issues (20)
- Is sercomp broken in v8.16? HOT 2
- How to handle "Needs option -impredicative-set." HOT 3
- installation HOT 4
- what version of coq serapi works with coq 8.10.2? HOT 9
- what is the best version of coq-serapi that works with coq 8.12? HOT 5
- Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 HOT 12
- Segfault on (Query () Goals) with sertop 8.15.0+0.15.3 HOT 4
- What is the purpose of coq-serapi's existance and why can't everything be done in coqtop? HOT 5
- Expose Section Variable Determining API in SerAPI HOT 6
- Incorrect goals when providing -topfile in sertop 8.10.0+0.7.2 HOT 2
- Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10 HOT 1
- Serlib testing needs to be improved.
- Missing conversion functions for types for the extraction plugin? HOT 3
- Can't run `make test` due to an error related to `eqType` HOT 4
- Windows PATH length (again) HOT 21
- macOS: serapi loads Coq .vo from compile time path HOT 4
- Run tests with MC 2 HOT 3
- Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01 HOT 5
- Segmentation fault in coq/getDocument call HOT 4
- New versioning scheme.
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from coq-serapi.