Bolton Bailey (Jan 29 2022 at 19:46): Bolton Bailey (Jan 29 2022 at 19:46):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?
Paolo Giarrusso (Jan 29 2022 at 20:03):Running eval $(opam env); dirname $(which coqtop) in a shell should print the right path to use.
Paolo Giarrusso (Jan 29 2022 at 20:04):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:
Paolo Giarrusso (Jan 29 2022 at 20:05):You should set coqtop.binPath as suggested in https://github.com/coq-community/vscoq#settings, but it sounds like you found more detailed instructions.
Karl Palmskog (Jan 29 2022 at 20:34):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.
Paolo Giarrusso (Jan 29 2022 at 21:01):... 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 :-)
Tim Carstens (Jan 29 2022 at 22:21):Bolton,
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).
Bolton Bailey (Jan 30 2022 at 02:39):Thanks, eval $(opam env); dirname $(which coqtop) worked to give me the directory for coqtop, and I can now step forward/backward in various files.
Bolton Bailey (Jan 30 2022 at 23:16):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?
Paolo Giarrusso (Jan 30 2022 at 23:20):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.
Paolo Giarrusso (Jan 30 2022 at 23:21):But IME all VsCoq does is remember the states that it has already shown you.
Paolo Giarrusso (Jan 30 2022 at 23:22):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.
Paolo Giarrusso (Jan 30 2022 at 23:22):(at least, that's my mental model of what I see, dunno if it's what actually happens)
Bolton Bailey (Jan 30 2022 at 23:35):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.
Paolo Giarrusso (Jan 31 2022 at 01:10):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.
Paolo Giarrusso (Jan 31 2022 at 01:11):Oh, (d) Coq cannot answer query AFAIK while updating the proof view. In part because the answers to the same queries can change.
Tim Carstens (Jan 31 2022 at 16:52):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
Tim Carstens (Jan 31 2022 at 16:53):alectryon has such a cache, for instance
Tim Carstens (Jan 31 2022 at 16:55):... 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 ;)
Karl Palmskog (Jan 31 2022 at 16:58):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)
Tim Carstens (Jan 31 2022 at 17:14):You are correct; I forgot about Coq's async mode
Karl Palmskog (Jan 31 2022 at 17:25):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
Paolo Giarrusso (Feb 01 2022 at 00:14):probably async proofs are more robust when driven from coqide, but as a vscoq user that sounds like a nightmare
Paolo Giarrusso (Feb 01 2022 at 00:14):let me know when the “stop Coq” button works reliably :-)
Paolo Giarrusso (Feb 01 2022 at 00:16):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…
Enrico Tassi (Feb 01 2022 at 07:38):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.
Paolo Giarrusso (Feb 01 2022 at 16:54):I'm then going to ask for an FAQ on OCaml 5 support, blockers and timelines — at least with coq-native disabled
Karl Palmskog (Feb 01 2022 at 17:39):did you see: https://twitter.com/ejgallego/status/1483436098227482626
People willing to experiment with @OCamlLang 's new shiny multicore in @CoqLang can find a PR adding 5.0 support to Coq here https://github.com/coq/coq/pull/15494 Things look really good, thanks to everyone who has helped make Coq run smoothly in 5.0!
- Emilio J. Gallego Arias (@ejgallego)Last updated: Jun 04 2023 at 23:30 UTC