Stream: Miscellaneous

Topic: Multithreaded coq/proofgeneral?


view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Mar 14 2021 at 15:43):

You can learn more about this mode in the CoqIDE chapter of the reference manual.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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: Aug 19 2022 at 19:03 UTC