Stream: VsCoq devs & users

Topic: About in VSCode


view this post on Zulip Ali Caglayan (Apr 26 2021 at 14:43):

Hi I am trying to use the About command in VScode but I don't see any output.

view this post on Zulip Ali Caglayan (Apr 26 2021 at 14:43):

The Output window pops up with the dropdown set to Queries

view this post on Zulip Ali Caglayan (Apr 26 2021 at 14:44):

There is also a Coq Language server log that I can veiw and things seem to be happening there

view this post on Zulip Ali Caglayan (Apr 26 2021 at 14:44):

Is it possible to set up an info window like in coqide?

view this post on Zulip Paolo Giarrusso (Apr 26 2021 at 14:45):

Might be because of a bug on first use

view this post on Zulip Paolo Giarrusso (Apr 26 2021 at 14:46):

I often have to either type About by hand, or change pane to the "error" pane

view this post on Zulip Paolo Giarrusso (Apr 26 2021 at 14:47):

not from Queries to Coq LS, but from the other panes on the side

view this post on Zulip Théo Winterhalter (Apr 26 2021 at 14:47):

For me at least Prompt About works. But sometimes the output is not shown and I have to close the pane and do it again.

view this post on Zulip Ali Caglayan (Apr 26 2021 at 17:00):

Yes this is because of first use

view this post on Zulip Ali Caglayan (Apr 26 2021 at 17:00):

restarting has fixed everything


Last updated: Jan 30 2023 at 17:03 UTC