Skip to content

Coqtop stderr output appears on the screen randomly #61

@felixbauckholt

Description

@felixbauckholt

When stepping through the following file (using Linux and Coq version 8.6), the string "<W> Grammar extension: in [constr:operconstr] some rule has been masked" appears on the screen at an unpredictable location:

Inductive natprod : Type :=
| pair : nat -> nat -> natprod.
Notation "( x , y )" := (pair x y).

This string doesn't move when scrolling through this file, so it doesn't seem like Vim is aware of its existence.

The appearing string doesn't seem to be in the coquille files, it looks like it's the output of Coqtop (see for example some of the output here: http://www.lix.polytechnique.fr/coq/pylons/logs/view/QuicksortComplexity/5528711275707690290).

Furthermore, this doesn't happen when I add stderr = subprocess.PIPE to the coqtop = subprocess.Popen(...) call in coqtop.py. So I think this message is from the stderr output of Coqtop.

I'll make a pull request to suppress this message shortly; any suggestions on how to use this message in a helpful way are welcome!

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions