Automatically generated goal names

[dhalilov]

This PR adds the possibility to have automatically generated goal names through the Generate Goal Names option. This also includes qualified goal names and showing the difference between focusable and non-focusable printing names in Show Existentials.

Requires #20813 to be merged first.

• Added / updated test-suite.
• Added changelog.
• Added / updated documentation.
  • Updated documented syntax by running make doc_gram_rsts.
• Opened overlay pull requests.

Overlays:

• Adapt to rocq-prover/rocq#20809 (Automatically generate goal names) stdlib#186
• Adapt to rocq-prover/rocq#20809 (use evar created by evar tactic instead of hard-coded name in unfold_post) PrincetonUniversity/VST#834
• Adapt to rocq-prover/rocq#20809. coq-tactician/coq-tactician#121

[ppedrot]

@coqbot run full ci

[coqbot-app]

🔴 CI failure at commit ca1c5f5 without any failure in the test-suite

✔️ Corresponding job for the base commit 90e3b7e succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-hott

• You can also pass me a specific list of targets to minimize as arguments.

[jfehrle]

Some details to consider.

It seems incomplete not to handle all tactics that introduce new goals, eg split.

Probably more comments later. Only so much I'm willing to do on my phone. I won't be near my computer until next week.

[jfehrle]

Why "fullyqualid"? Are you prohibiting use of the shortest unique suffix? If so, that behavior is inconsistent with all other qualids--and give your rationale.

Also I didn't see a description of this nonterminal in the doc---IMO that's a requirement.

[dhalilov]

Qualified goal names behave differently from other qualids, since there is only one name for them which is the shortest one by construction. That means they are also always fully qualified, so I think fullyqualid makes the distinction clear.

[jfehrle]

Qualified goal names behave differently from other quali

That's precisely the problem. While the syntax is the same as qualids, their behavior/use is entirely different. Just call them goal names and explain that they may have multiple dotted components.

[dhalilov]

It seems incomplete not to handle all tactics that introduce new goals, eg split.

split does not work at the moment because conj (constructor of and) does not have named hypotheses, so no names cannot be generated. Could be changed in another patch.

[dhalilov]

(Cleaned the history. The PR needs #20813 to be merged first and then will be rebased on master)

[jfehrle]

The PR needs #20813 to be merged first and then will be rebased on master)

Best to put this in the PR description--reviewers are likely to miss this if it's only in the conversation.

[ppedrot]

The low-level code changes look fine to me. I think that the flag should be opt-in though, this is already hinted at by the documentation. I can take care of this myself by tweaking the commit that introduces it though.

[ppedrot]

For some reason, tactician now seems to require an overlay.

[ppedrot]

@coqbot merge now

[coqbot-app]

@ppedrot: Please take care of the following overlays:

• 20809-ppedrot-autonaming-goals.sh

[ppedrot]

@dhalilov finally merged, thanks for your patience!

[dhalilov]

Many thanks for the help and reviews! 🥳