Stream: VsCoq devs & users

Topic: Beginner: exploring features


view this post on Zulip 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:

Thanks a bunch!

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (Apr 02 2021 at 15:37):

Is it possible that your tactic admits stuff?

view this post on Zulip Pierre Vial (Apr 06 2021 at 07:05):

Yes, absolutely. This is it, then. Thanks !


Last updated: Jan 30 2023 at 18:04 UTC