Strict behavior for hint databases about stdlib2 HOT 8 OPEN

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.

from stdlib2.

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 *.

from stdlib2.

@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?

from stdlib2.

@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.

from stdlib2.

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

from stdlib2.

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

from stdlib2.

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?

from stdlib2.

Please open the issue.

from stdlib2.