Set Warnings misbehaves in IDEs (with async proofs?)

[Blaisorblade]

Description of the problem

Set Warnings doesn't seem to work correctly with async proofs in VsCoq (and maybe elsewhere) — neither the location nor undoing side effects work correctly. It's hard to describe exactly what happens, but here are partial results from some experiments:

Undoing Set Warnings by stepping back doesn't undo its side effects correctly. And this snippet gives different results depending on how you step through it:

Require Import ssreflect.
Set Warnings "-ssr-search-moved".
Search "++".

Going step-by-step works correctly. When jumping to the end, you get a warning, seemingly because Search is run with the warning enabled.

Also, the location of the warning seems sometimes wrong — it's never attached to Search, but it seems to the previous statement (even when single-stepping) — preventing undo from doing its job correctly. The same happens also in:

Require Import Bool.
Require Import ssreflect.
Require Import Lists.List.
Definition foo := 1.
Search "++".

Coq Version

8.12.1

[Zimmi48]

I'm not surprised that among all options, it is Warnings that doesn't behave. It is somewhat a black sheep in the sense that contrary to all other int or string-valued options, it has an append semantics and cannot be Unset.

The location issue is probably separate and unrelated to the Undo issue.

[Blaisorblade]

The location issue is probably separate and unrelated to the Undo issue.

Possibly, but I can't write a report good enough for those deductions, you'd need somebody who knows the internals.

[SkySkimmer]

Cannot reproduce with recent coq
(tested with

Set Warnings "-unused-pattern-matching-variable".

Check match _ with true => true | False => false end.

since the Search warning doesn't exist anymore)