Strict behavior for hint databases

[Zimmi48]

Since Stdlib2 will also mean rethinking the hint databases, what about setting the Loose Hint Behavior option to "Strict"? cc rocq-prover/rocq#7710

[andres-erbsen]

This sounds great. I would propose to systematically rule out use of auto with * using something like this

(** [intuition] means [intuition auto with *].  This is very wrong and
    fragile and slow.  We make [intuition] mean [intuition auto]. *)
Tactic Notation "intuition" tactic3(tactic) := intuition tactic.
Tactic Notation "intuition" := intuition auto.

(** [firstorder] means [firstorder auto with *].  This is very wrong
    and fragile and slow.  We make [firstorder] mean [firstorder
    auto]. *)
Global Set Firstorder Solver auto.

(** A version of [intuition] that allows you to see how the old
    [intuition] tactic solves the proof. *)
Ltac debug_intuition := idtac "<infomsg>Warning: debug_intuition should not be used in production code.</infomsg>"; intuition debug auto with *.

[maximedenes]

@ppedrot I'd like to hear what you'd suggest us to do. I would strongly be in favor of stdlib2 not depending on the lax hint behavior, indeed. On the other hand, I'd like to not impact downstream developments.

Is there a way to set the option at the level of a project?

[Zimmi48]

@maximedenes Yes, there is now (and we should deprecate Global Set and tell people to use this instead). You can set an option through a command-line flag. Then, let's say you use Dune as your build system, you can set a flag to compile your project using the (flags ...) stanza within the (coq.theory ...) one.

[ppedrot]

Note that I think we are missing half of the tools for this. The option prevents the caller from depending on hints that were not required, but there is no way for the library author to prevent their hints not to be available through a require. I believe we should introduce another option for this behaviour, which could be turned on by default in any new development.

[maximedenes]

Yeah, I just realized that. The current situation is very strange, people writing hints can't control their locality.

[ppedrot]

Technically, it shouldn't even be the responsibility of the hint writer, because this super-global behaviour is clearly a bug...

[maximedenes]

Technically, it shouldn't even be the responsibility of the hint writer, because this super-global behaviour is clearly a bug...

Yes, but what I mean is if we want people to migrate to a saner default, the option you are talking about now would have been more useful than the one we have currently, IMHO.

Should I open an issue for the new option?

[ppedrot]

Please open the issue.