Is there a way to use more threads in coq/proofgeneral? Do I need to pass a flag in _CoqProject? (new to both Coq and Zulip, sorry if this is too trivial -- I'd be happy to learn about better places to ask these kinds of questions.)
Coq has an async mode but it is not supported in standard proof general. There's an experimental async branch that does support it though.
You can learn more about this mode in the CoqIDE chapter of the reference manual.
What's the status of vscode support? I understood the vscode protocol was a bit better suited for this.
We just re-started putting effort on a LSP based vscoq backend (it had a big pause mainly because of the pandemic). Here the current repo vscoq-language-server, but it will likely be moved/renamed this week, so it's not a very relevant pointer.
GitHub repos that get moved / renamed get automatic redirections. It's not a relevant pointer only if you delete and recreate the repo.
Thanks for the pointer @Théo Zimmermann -- I'm noticing that proofgeneral is much slower than coqide: is this because of async mode?
I'm not sure. When jumping through long files, certainly. But if you notice a more general slowness, it may be something else...
okay, I will keep an eye out, then. Currently just trying to get started learning coq and don't want to fiddle too much. Thank you!
Last updated: May 31 2023 at 09:01 UTC