How to activate the Coq messages in vscode/vscoq like in the CoqIde/jscoq?

Question

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://github.com/coq-community/vscoq/issues/280
• https://coq.discourse.group/t/how-to-activate-the-messages-window-in-vscode-like-the-coqide-has/1584

Answer 1

Seems it's printed in:

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