search

coq / stdlib2

GNU Lesser General Public License v2.1
39 stars 9 forks source link

Strict behavior for hint databases #6

Open Zimmi48 opened 6 years ago

Zimmi48 commented 6 years ago

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

andres-erbsen commented 6 years ago

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 commented 4 years ago

@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 commented 4 years ago

@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 commented 4 years ago

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 commented 4 years ago

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

ppedrot commented 4 years ago

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

maximedenes commented 4 years ago

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 commented 4 years ago

Please open the issue.