Paolo Giarrusso (Dec 13 2020 at 20:41): Paolo Giarrusso (Dec 13 2020 at 20:41):IIUC, Set Warnings doesn't seem STM-aware. In VsCoq, undoing it 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.
Paolo Giarrusso (Dec 13 2020 at 20:48):Oh sorry... 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
Require Import Bool.
Require Import ssreflect.
Require Import Lists.List.
Definition foo := 1.
Search "++".
Why not report this as a bug?
Paolo Giarrusso (Dec 15 2020 at 12:54):ack. filed https://github.com/coq/coq/issues/13637; not a great report but better than nothing
Last updated: Apr 19 2024 at 18:01 UTC