My emacs froze one too many time, I decided to give a shot at VsCoq, but am totally new to VSCode in general. I have a couple of questions:
coq. That got me quickly on track to find features that obviously map to the PG/company-coq ones. However there are some that are a bit mysterious to me (
Finish Computationsfor instance): is there a way to read their
docstring? There appear to be some in the Json by looking on the github, but I can't find how to display them.
LtacProf results treeview, which I gathered refer to the
View ltac Profilecommand. However here again I can't find a doc, and trying to randomly use it gets me an output with
total time : 0.000sand a cute empty array, but I can't seem to figure out how it works. Is it documented somewhere?
Thanks a bunch!
I think that "Finish Computations" has to do with parallel proof processing and "Qed" (like in CoqIDE) but I wasn't able to make it work.
I don't know how to color the search results either, that would be a great feature to have!
+1 for syntax coloring of the output, that's the main reason I have trouble committing to VsCoq permanently
I tried the bullet in different places, but it didn't work.
Unshelvedoes not produce anything in any window apparently :(
Is it by chance possible that it is related to the plugin ?
If I'm not mistaken this message "There are unfocused goals" might mean that some goals have been admitted.
Is it possible that your tactic admits stuff?
Yes, absolutely. This is it, then. Thanks !
Last updated: Jan 30 2023 at 18:04 UTC