Stream: Coq users

Topic: `Set Warnings`, `Search` warnings, and STM


view this post on Zulip 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 "++".

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 20:42):

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

view this post on Zulip 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 "++".

view this post on Zulip Théo Zimmermann (Dec 14 2020 at 08:30):

Why not report this as a bug?

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC