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.

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

Please add an option to prevent vscoq from preemptively invoking coq #1057

Open
JasonGross opened this issue Mar 3, 2025 · 2 comments
Open

Comments

@JasonGross
Copy link
Member

When I load a large file, vscoq is often unresponsive for many sections, presumably while it's sending the document off for parsing. Is there a way to avoid this, and have it only be triggered when I evaluate to point

@gares
Copy link
Member

gares commented Mar 3, 2025

What do you mean by non responsive? I mean, what are you asking vscoq to do while it is presumably parsing the large file?

@rtetley
Copy link
Collaborator

rtetley commented Mar 3, 2025

How large a file are we talking ? Even the infamous Pff.v which is almost 30 000 lines long takes about 2 to 3 seconds to parse on my setup. Could you give us some more details ?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants