Export locality for all hint commands#13388
Export locality for all hint commands#13388coqbot-app[bot] merged 3 commits intorocq-prover:masterfrom
Conversation
9bef5b7 to
f04c963
Compare
There was a problem hiding this comment.
LGTM (I've reviewed the PR in full and can be the assignee if needed).
I'm just wondering if the locality attributes should not also be supported by the Create HintDb command. Currently, it is superglobal and it's not innocuous since Create HintDb changes the default transparency compared to an implicitly created hint database. Furthermore, it is my impression that supporting the locality attributes for this command as well would lead to a lot of code factorization. Up to you...
doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst
Outdated
Show resolved
Hide resolved
|
Create HintDb is purposely left with a superglobal semantics. Since hint databases do not have qualified names but mere strings, it doesn't make sense to ask them to follow an Import-scoped semantics. One day maybe we'll learn not to give mere strings as user-facing objects identifiers... |
|
(The proper fix for this command is to give kernel names to hint databases, but it's a change that's way bigger than the current PR, and that will entail amongst other backwards incompatibility.) |
|
Sounds good to me. |
f04c963 to
7e55f48
Compare
|
Given the upcoming freeze, let's be proactive. I'm self-assigning and announcing that I will merge this PR on Monday 16th (tomorrow) noon if there are no more comments in the meantime. |
|
please go |
|
@coqbot: merge now |
|
I just noticed, what about |
|
Hint Rewrite uses a different database mechanism, so the plan does not apply. |
|
BTW, this is super confusing that |
|
It is a command of the hint family: to the user that is not confusing at all. The implementation is confusing though, and we should certainly merge the bases here, accepting rewrite lemmas and resolution lemmas in the same database. There could certainly be some uses of developping proof-search up-to rewriting automation based on them. The rewrite hint databases need the same set-theoretic operations than the "lemma" hint databases too. |
|
@ppedrot what I meant is, do they also have superglobal status by default? |
Yes, they do look superglobal by default indeed.
Not only the implementation. Even the documentation of that command is part of another subsection of the automation chapter. |
I call this confusing: Hint Rewrite plus_O_n : foo.
Fail Print HintDb foo.
(*
The command has indeed failed with message:
No such Hint database: foo.
*)
Great! Can we get a roadmap for the hint database system? It will certainly influence the documentation as well (the current status is terrible, so I really want to change it but it would be stupid to change it in a way that is not consistent with this roadmap). |
This is completing the implementation of export locality for the
Cut,Mode,Transparent / OpaqueandRemove Hintscommands. This is necessary for a satisfying implementation of #13384 where we don't have to do half the job for some commands and delay the groundwork for a future fix to a later release.As such, dear assignee and RMs, this is high priority for 8.13. Sorry for being pushy at the last moment, although this is quite usual in the dev process...