search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
33 stars 2 forks source link

[WIP] Add an option: Set/Unset Algebra Tactics Debug #46

Closed pi8027 closed 2 years ago

pi8027 commented 2 years ago

@gares Apparently, Require Import lib does not make an option added by lib using coq.option.add available. I will open an issue.

gares commented 2 years ago

I see. Anyway, for debug it is better to use another API which I shall bound

gares commented 2 years ago

Are you sure a #[debug] or #[verbose] attribute would not be better?

pi8027 commented 2 years ago

Ah, using the attribute mechanism is indeed better. I will try to implement that.

pi8027 commented 2 years ago

@gares It seems that tactic notations cannot take attributes. Do I miss something? https://github.com/math-comp/algebra-tactics/blob/d2882619a5ee9f98fd0b92c3efb8d82eac396bb0/theories/ring.v#L705-L706

gares commented 2 years ago

some limitations: https://github.com/LPCIC/coq-elpi#attributes

gares commented 2 years ago

Now that I think about it, if you pick a different syntax for the delimiter, then there is no conflict... but yea, not super nice :-/