Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[fleche] [lsp] Speculative execution #593

Closed
ejgallego opened this issue Nov 5, 2023 · 1 comment
Closed

[fleche] [lsp] Speculative execution #593

ejgallego opened this issue Nov 5, 2023 · 1 comment
Labels
kind: enhancement New feature or request kind: internal part: flèche part: lsp server part: protocol (custom)
Milestone
0.1.9

Comments

@ejgallego
Copy link
Owner

We want to implement a new request coq/execute that can run a Coq vernacular in a particular context, without altering the document. The answer to this request should be all the information we have gathered from the execution.

There is a prototype already used by the pretac goals option (cc #574) , but we need to finish the Flèche API, and bind to the LSP protocol.
@ejgallego ejgallego added the kind: bug Something isn't working label Nov 5, 2023
@ejgallego ejgallego added this to the 0.1.9 milestone Nov 5, 2023
@ejgallego
Copy link
Owner Author

Fixed in #600 and #601 ; further improvements can be tracked on new issues.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: enhancement New feature or request kind: internal part: flèche part: lsp server part: protocol (custom)
Projects
None yet
Milestone
0.1.9
Development

No branches or pull requests
1 participant
@ejgallego