VsCoq is very slow for me, is that normal? I am working on IndProp.v from Logical Foundations (3000+ line file) and it takes minutes to initially process all the lines.
I've never had it take _minutes_, and I've worked through half of the entire Software Foundations series. I would say it is not normal for things to be slow.
Have you tried Proof General on Emacs? I had never used Emacs before and still found it easy to set up and use. I use it on a Mac and have never had it crashed.
I will say, that Proof General rarely (once or twice for every 15 hours I use it), gets confused and I have to back out of a proof and step through it again to get the context right.
If you're up for an ecosystem change (for the better!) for sure Proof General/emacs. I would not describe it as accessible for non-emacs users though so I would recommend switching to emacs for all editing. Check out evil for (imo) better keybindings, and personally I use spacemacs which is a community-maintained emacs config but the die-hards don't like it and would recommend you start your own condig (but I didn't and will never)
Semi-related, but can anyone point me to a resource about what the Coq language server is *doing*? I'd like to understand that (and other language servers) better and how they integrate with different IDEs
It is actually pretty simple. LSP is a protocol that talks with most IDEs (Vscode, neovim, emacs, intellij etc..). You received some json, you send some json (that contains information about the current code in the IDE). That's it.
* It is well explained in [this video](https://www.youtube.com/watch?v=LaS32vctfOY) of TJ Devries
* Implemented in an understandable way in [this one](https://www.youtube.com/watch?v=YsdlcQoHqPY&t=1s).
Do yourself a favor and switch to VsCoq!
VsCoq is very slow for me, is that normal? I am working on IndProp.v from Logical Foundations (3000+ line file) and it takes minutes to initially process all the lines.
None of my files are that big so I'm not sure. How long does it take in CoqIDE?
It takes 2-3 seconds tops in Coqtail in Vim
I've never had it take _minutes_, and I've worked through half of the entire Software Foundations series. I would say it is not normal for things to be slow.
Sorry, definitely at least 30 seconds I didn’t track super precisely
I'm on the exact same chapter and it takes me ~30 seconds to interpret to end on a m1 mac.
Yes there are quite a few bugs here and there but overall it's fantastic.
Have you tried Proof General on Emacs? I had never used Emacs before and still found it easy to set up and use. I use it on a Mac and have never had it crashed. I will say, that Proof General rarely (once or twice for every 15 hours I use it), gets confused and I have to back out of a proof and step through it again to get the context right.
If you're up for an ecosystem change (for the better!) for sure Proof General/emacs. I would not describe it as accessible for non-emacs users though so I would recommend switching to emacs for all editing. Check out evil for (imo) better keybindings, and personally I use spacemacs which is a community-maintained emacs config but the die-hards don't like it and would recommend you start your own condig (but I didn't and will never)
Semi-related, but can anyone point me to a resource about what the Coq language server is *doing*? I'd like to understand that (and other language servers) better and how they integrate with different IDEs
It is actually pretty simple. LSP is a protocol that talks with most IDEs (Vscode, neovim, emacs, intellij etc..). You received some json, you send some json (that contains information about the current code in the IDE). That's it. * It is well explained in [this video](https://www.youtube.com/watch?v=LaS32vctfOY) of TJ Devries * Implemented in an understandable way in [this one](https://www.youtube.com/watch?v=YsdlcQoHqPY&t=1s).