Skip to content

[BUG] Set Silent and -quiet have no effect #1210

Description

@cpitclaudel

Describe the Bug

Running Set Silent does not change the value of the Silent flag. Nor does passing -quiet. In both cases, verbose messages are still printed.

To Reproduce

Run the following code in VSRocq, with and without -quiet in "vsrocq.args":

Definition a := 1.

Test Silent.
Unset Silent.
Test Silent.
Set Silent.
Test Silent.

Definition b := 1.

Expected vs. Actual Behavior

All Test Silent lines, with or without -quiet, say Silent is off. Both Definition lines print … is defined.

Debug Information Value
Rocq Installation The Rocq Prover, version 9.2+rc2 compiled with OCaml 5.4.0
Rocq Path /home/cpc/.opam/rocq-9.2/lib/coq
VsRocq Extension Version 2.3.4
VsRocqTop Version 2.3.4
VsRocqTop Path /home/cpc/.opam/rocq-9.2/bin/vsrocqtop
OS x64 linux
VSCode Version 1.109.3

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions