Sam Stites (Mar 14 2021 at 15:13): Sam Stites (Mar 14 2021 at 15:13):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.)
Théo Zimmermann (Mar 14 2021 at 15:42):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.
Théo Zimmermann (Mar 14 2021 at 15:43):You can learn more about this mode in the CoqIDE chapter of the reference manual.
Bas Spitters (Mar 14 2021 at 15:45):What's the status of vscode support? I understood the vscode protocol was a bit better suited for this.
Enrico Tassi (Mar 14 2021 at 18:35):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.
Théo Zimmermann (Mar 14 2021 at 18:48):GitHub repos that get moved / renamed get automatic redirections. It's not a relevant pointer only if you delete and recreate the repo.
Sam Stites (Mar 14 2021 at 19:52):Thanks for the pointer @Théo Zimmermann -- I'm noticing that proofgeneral is much slower than coqide: is this because of async mode?
Théo Zimmermann (Mar 14 2021 at 19:53):I'm not sure. When jumping through long files, certainly. But if you notice a more general slowness, it may be something else...
Sam Stites (Mar 14 2021 at 19:55):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: Oct 13 2024 at 01:02 UTC