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

Incremental and Unsaved Support #128

Open
michaelmesser opened this issue Dec 29, 2021 · 1 comment
Open

Incremental and Unsaved Support #128

michaelmesser opened this issue Dec 29, 2021 · 1 comment
Labels
enhancement New feature or request feature: text synchronization performance status: blocked by Idris Requires changes to the Idris API

Comments

@michaelmesser
Copy link
Contributor

michaelmesser commented Dec 29, 2021 •
edited
Loading

Ideally we would support check as you type, but this require incremental type checking and unsaved file support in the Idris API. This would also allow diagnostics to be reported with a version. Haskell LSP's uses a VFS. Blocked by idris-lang/Idris2#1187.
@michaelmesser michaelmesser pinned this issue Jan 19, 2022
@michaelmesser michaelmesser unpinned this issue Feb 12, 2022
@michaelmesser michaelmesser pinned this issue Mar 25, 2022
@michaelmesser
Copy link
Contributor Author

michaelmesser commented Mar 25, 2022 •
edited
Loading

As far as I can tell the best way to solve this is to rewrite Idris to use a system similar to Rust's salsa. An example of something similar in Haskell is described in this blog and this video.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request feature: text synchronization performance status: blocked by Idris Requires changes to the Idris API
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@michaelmesser