The messages bar is missing?

[brando90]

I am expecting something in my messages bar but I don't see it

Example script:

Fixpoint add_left (n m : nat) : nat :=
  match n with
  | O => m
  | S p => S (add_left p m)
  end.
  
Lemma demo_1 :
  forall (n : nat),
    add_left n O = n.
Proof.
  intros.                                     (* goal : add_left n O = n *)  
  let add_left_red := eval red in add_left in (* reduce add_left, but leave goal alone *)
  idtac add_left_red.                         (* print the result *)
  (* Print eval. gives error *) 
  Print red.
  Print add_left_red.
  admit.
Abort.

in JScoq I see (https://coq.vercel.app/scratchpad.html):

(fix add_left (n m : nat) {struct n} : nat :=
  match n with
| 0 => m
| S p => S (add_left p m)
end)

in vscode I see nothing.

See pics for clarity

cross: https://coq.discourse.group/t/how-to-activate-the-messages-window-in-vscode-like-the-coqide-has/1584
https://stackoverflow.com/questions/71352672/how-to-activate-the-coq-messages-in-vscode-vscoq-like-in-the-coqide

[Zimmi48]

Hey @brando90, I've noticed that you're used to cross-posting the same questions on multiple channels, but this is not a recommended practice as this makes it harder for others to follow the discussion. Most people are active on all these channels, so they will see all your messages and will decide to answer here or there and other people won't see their answers.

So for instance, if you are sure that something is a bug, then you should report it only in the proper bug tracker. But if you are not sure, then you should only use Discourse or Zulip to ask whether it is a bug, and if people tell you it is, then open an issue. And if something is clearly just a question whose answer might be useful to others, then post it on StackOverflow or Discourse.

In this case, it does look like a bug to me that messages from idtac do not appear in the "Output" of VsCode.

[TheoWinterhalter]

It's not a bug, it's not printed in "Notices" but in "Info".

[Zimmi48]

Oh, right! But how are users supposed to discover the various types of output and how to switch between them?

[TheoWinterhalter]

I don't know to be honest.

[rtetley]

This does not seem to be working in VsCoq 2, I will keep it open to investigate. I would expect the message to appear in the messages section of the Goal panel.

[rtetley]

Solved by #842