Hello I am a beginner with Coq who is looking to explore Coq a bit. I have followed the installation from opam instructions and cloned math-comp, but when I start the project folder in VSCode, and I enter a file the project in VSCode and try the "Coq: Step Forward" command, I get error "Could not start coqtop (coqtop)". Should I follow the instructions for "Set path for this project"? What should I set the path to?
eval $(opam env); dirname $(which coqtop) in a shell should print the right path to use.
Should I follow the instructions for "Set path for this project"? What should I set the path to?
you usually have to give that path to VsCoq, so I _guess_ yes, but I'm not sure which instructions you mean :sweat_smile:
You should set
coqtop.binPath as suggested in https://github.com/coq-community/vscoq#settings, but it sounds like you found more detailed instructions.
also of note, it's not recommended to learn Coq from scratch by playing around with the MathComp library itself (which is a fairly complex project). Consider one of the books, e.g., the MathComp book and its library.
... and many people are arguably even better off starting from https://softwarefoundations.cis.upenn.edu/, depending on their goals — but if you'd like advice for your goals, please ask a new question and state your interests :-)
Which OS are you using, and how did you install Coq?
On Linux, I installed Coq using opam. Then I launch vscode from an environment where the opam env variables have been set. With this setup, everything vscode/vscoq needs will be in the search path.
On Windows, I understand that people like to use the Coq Platform (which provides its own installer for Coq). I don't have experience with this personally but there are people here who do
I'll mention that I also routinely use vscode/vscoq in "remote development" mode. In this mode you basically connect to a Linux or Docker host. This works great if you have a Linux server with opam installed, or perhaps a Docker image (such as those provided by coq-community).
eval $(opam env); dirname $(which coqtop) worked to give me the directory for
coqtop, and I can now step forward/backward in various files.
I'm noticing that the "Coq: View the proof-state at the cursor position" command doesn't seem to work. I expect to be able to place my cursor somewhere and call this command and have it be just like I had called "Step Forward" a bunch of times to get to that position. Currently it just does nothing. Am I right about how this is supposed to work?
I haven't used that command but I don't think it can work like that; you rather want "Interpret to point"... but you can move your cursor before the end of the interpreted area, and you'll see the previous state.
But IME all VsCoq does is remember the states that it has already shown you.
so if you jump over a region using "Interpret to point" rather than lots of "step forward" (or the appropriate keyboard shortcut), you won't be able to see the intermediate states, because VsCoq itself never received the data.
(at least, that's my mental model of what I see, dunno if it's what actually happens)
I guess my ideal would be something more like Lean where you don't have to input any commands, you just put your cursor somewhere and the proofview automatically updates. Not sure if there are internal differences between Coq and Lean that make this infeasible but I guess it would make a good feature request.
Dunno internals, but my 2 cents it that the Coq externals would make it terrible. I want to move my cursor without causing (a) errors (b) infinite loops (c) other problems that are more complex to explain.
Oh, (d) Coq cannot answer query AFAIK while updating the proof view. In part because the answers to the same queries can change.
I think Lean is caching states; it would surprise me greatly if every time you moved the cursor the Lean engine was re-evaluating tactics
alectryon has such a cache, for instance
... but it is also true that Lean's implementation is tightly optimized for modern dev workflows in ways that other tools are not. Except for the backwards compatibility thingy, of course ;)
the original "asynch processing" ITP is Isabelle(/HOL). I'm pretty sure Coq can support this click-in-middle model, but it would have to be a layer on top of something like SerAPI (e.g., Emilio's unreleased document API that he discusses here)
You are correct; I forgot about Coq's async mode
there are two "views" of asynch proofs. One is the IDE-oriented one discussed here, but I there is also the batch view of asynch proofs. With a properly annotated project, one can get a lot of batch proof-checking speedups by the combination of asynch+parallelism (as per here), orthogonally to fast clicks inside the IDE
probably async proofs are more robust when driven from coqide, but as a vscoq user that sounds like a nightmare
let me know when the “stop Coq” button works reliably :-)
a colleague mentioned that he learned some tricks for the XML protocol from the coqide sources (and it does feel more stable), but I’m not sure that’s perfect…
These reliability problems are deep in OCaml. Things will be better with OCaml 5, and the native lsp backend which hopefully will see the light before the fall.
For example interruptibily/fairness of scheduling was non existend in OCaml before multicore. So the stop button was bagging the pity of the allocator and the os scheduler at the same time.
I'm then going to ask for an FAQ on OCaml 5 support, blockers and timelines — at least with coq-native disabled
did you see: https://twitter.com/ejgallego/status/1483436098227482626
Last updated: Jan 30 2023 at 18:04 UTC