Skip to content

[BUG] > Print does nothing #1225

@mattam82

Description

@mattam82

IMPORTANT: Before You Submit This Issue

Describe the Bug

I can't see the output of interactive > Rocq: Print / > Rocq: About commands anywhere and Rocq: Add Tab seems to have no effect either to show the query panel where presumably I should see the results.

To Reproduce

Steps to reproduce the behavior:

  1. Open a .v file
  2. Definition a := 0.
  3. In the command pallette: > Rocq: Print a
  4. Nothing happens

Environment (paste the result of Rocq: Troubleshooting: Show Setup):

Debug Information Value
Rocq Installation The Rocq Prover, version 9.3+alpha compiled with OCaml 5.4.1
Rocq Path /Volumes/Dev/rocq/rocq-univs/_build/install/default/lib/coq
VsRocq Extension Version 2.3.4
VsRocqTop Version 2.3.4
VsRocqTop Path _build/install/default/bin/vsrocqtop
OS x64 darwin
VSCode Version 1.113.0

Rocq Log Output (if applicable)

Nothing in Rocq Log
In VsRocq:


[GoalPanel] Rendered in current panel
[GoalPanel] Received proofview notification
[GoalPanel] Rendered in current panel
[GoalPanel] Received proofview notification
[GoalPanel] Rendered in current panel
[GoalPanel] Received proofview notification
[GoalPanel] Rendered in current panel
[GoalPanel] Received proofview notification
[GoalPanel] Rendered in current panel
[GoalPanel] Received proofview notification
[GoalPanel] Rendered in current panel
[DocumentStateViewProvider] Getting document state for uri: file:///Volumes/Dev/rocq/rocq-univs/test-suite/success/telescopes_variances.v
[DocumentStateViewProvider] Firing event
[DocumentStateViewProvider] Current doc uri: file:///Volumes/Dev/rocq/rocq-univs/test-suite/success/telescopes_variances.v
[DocumentStateViewProvider] Getting document state for uri: file:///Volumes/Dev/rocq/rocq-univs/test-suite/success/telescopes_variances.v

If the issue involves a server crash or unexpected Rocq behavior, please provide logs from the "Rocq Language Server" output channel in VS Code.

Nothing happens in the Rocq Language Server, Rocq Log or VsRocq output panes when issuing Print/About commands, even with -vsrocq-d all on.

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions