Yannick Zakowski (Mar 30 2021 at 18:31): Yannick Zakowski (Mar 30 2021 at 18:31):Hello,
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 Computations for 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 Profile command. However here again I can't find a doc, and trying to randomly use it gets me an output with total time : 0.000s and a cute empty array, but I can't seem to figure out how it works. Is it documented somewhere?Thanks a bunch!
Théo Zimmermann (Mar 30 2021 at 18:35):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.
Matthieu Sozeau (Mar 31 2021 at 08:12):I don't know how to color the search results either, that would be a great feature to have!
Yannick Forster (Mar 31 2021 at 09:59):+1 for syntax coloring of the output, that's the main reason I have trouble committing to VsCoq permanently
Pierre Vial (Apr 02 2021 at 15:34):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 ?
Théo Winterhalter (Apr 02 2021 at 15:36):If I'm not mistaken this message "There are unfocused goals" might mean that some goals have been admitted.
Théo Winterhalter (Apr 02 2021 at 15:37):Is it possible that your tactic admits stuff?
Pierre Vial (Apr 06 2021 at 07:05):Yes, absolutely. This is it, then. Thanks !
Last updated: Apr 19 2024 at 20:01 UTC