btauto should not modify core HintDb

[samuelgruetter]

Today I added a seemingly innocent Require Import Coq.btauto.Btauto. at the top of a file, and this change broke a proof script further down in that file.

It turns out this happened because btauto adds the following Hint to core:

https://github.com/coq/coq/blob/9193769161e1f06b371eed99dfe9e90fec9a14a6/theories/btauto/Algebra.v#L3-L13

This hint is certainly useful, but it's unfortunate that it's in a not-always-imported file, because it makes developments very brittle, as described in the scenario above.

Is there a "policy" regarding which files are "allowed" to add hints to core?

Coq version: 8.11.0, master

[Zimmi48]

Is there a "policy" regarding which files are "allowed" to add hints to core?

There's no written down policy, but judging from some recent PRs, there is a will to extract as much as possible out of the core database.

[Zimmi48]

OTOH, if your script broke because auto was suddenly more successful, maybe that says something about the robustness of your proof style...

[samuelgruetter]

OTOH, if your script broke because auto was suddenly more successful, maybe that says something about the robustness of your proof style...

That's indeed what happened. I wasn't optimizing for robustness, but for prototyping speed and proof-script debuggability. Are you implying that this is a "wontfix because user is not using Coq in the intended way?"

[Zimmi48]

I won't be the one to decide anyway. I don't know what @coq/stdlib-maintainers think of this.

I am concerned with that moving this hint in a new database would mean that users would completely stop benefiting from it. However, a compromise might be to move it to some existing database like datatypes...