Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Make focus command and goal selection for query commands independent of ltac1 #18707

Merged
merged 1 commit into from Mar 26, 2024
Merged

Make focus command and goal selection for query commands independent of ltac1 #18707

merged 1 commit into from Mar 26, 2024

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Feb 22, 2024 •
edited

@SkySkimmer SkySkimmer added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. labels Feb 22, 2024
@SkySkimmer SkySkimmer added this to the 8.20+rc1 milestone Feb 22, 2024
@SkySkimmer SkySkimmer requested review from a team as code owners February 22, 2024 15:40
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Feb 22, 2024
@SkySkimmer SkySkimmer force-pushed the vernac-focus branch 2 times, most recently from dc8dfbf to 6c416d5 Compare February 22, 2024 16:01
@SkySkimmer SkySkimmer requested a review from a team as a code owner February 22, 2024 16:01
@ppedrot ppedrot self-assigned this Feb 22, 2024
@SkySkimmer SkySkimmer added the needs: fixing The proposed code change is broken. label Feb 27, 2024
@SkySkimmer
Copy link
Contributor Author

It doesn't factorize properly, not sure how to fix.
There's query_command, { and arbitrary tactics which can be preceded with a toplevel selector. Arbitrary tactics also support par:, and their grammar is only active in proof mode.

@SkySkimmer SkySkimmer requested a review from a team as a code owner March 14, 2024 14:20
SkySkimmer
SkySkimmer commented Mar 14, 2024
View reviewed changes
plugins/ltac/g_ltac.mlg
| g = OPT toplevel_selector; "{" -> { Vernacexpr.VernacSynPure (Vernacexpr.VernacSubproof g) } ] ]
[ [ p = subprf -> { Vernacexpr.VernacSynPure p }
| g = OPT toplevel_selector; p = subprf_with_selector -> { Vernacexpr.VernacSynPure (p g) }
] ]
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe adding these 2 rules could/should be automated in register_proof_mode? Not in this PR though I think.

@SkySkimmer SkySkimmer removed the needs: fixing The proposed code change is broken. label Mar 14, 2024
@SkySkimmer
Copy link
Contributor Author

I think it works now, although the proof modes need to manually coordinate so eg it won't automatically work with mtac2 (but should be easy to adapt mtac2?)

SkySkimmer added a commit to SkySkimmer/Mtac2 that referenced this pull request Mar 14, 2024
@SkySkimmer
Adapt to coq/coq#18707 (proof mode needs to cooperate with subprf gra…
b18ff96 
…mmar)
@SkySkimmer
Copy link
Contributor Author

@coqbot run full ci

@coqbot-app coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 14, 2024
@SkySkimmer SkySkimmer added the needs: test-suite update Test case should be added to / updated in the test-suite. label Mar 14, 2024
@SkySkimmer
Copy link
Contributor Author

Test suite failure is because an interp time error became a parsing error (which can't be caught by Fail). We just need to turn the test into an output test.

@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: test-suite update Test case should be added to / updated in the test-suite. labels Mar 25, 2024
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 25, 2024
@ppedrot
Copy link
Member

ppedrot commented Mar 26, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 0bb8d19 into coq:master Mar 26, 2024
6 checks passed
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Mar 26, 2024

@ppedrot: Please take care of the following overlays:

  • 18707-SkySkimmer-vernac-focus.sh

Janno added a commit to Mtac2/Mtac2 that referenced this pull request Mar 26, 2024
@Janno
Merge pull request #399 from SkySkimmer/vernac-focus
919348a 
Adapt to coq/coq#18707 (proof mode needs to cooperate with subprf grammar)
@SkySkimmer SkySkimmer deleted the vernac-focus branch March 27, 2024 12:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

Ltac2 does not support focus command with goal selector (1:{ etc) Shared proof mode grammar
2 participants
@SkySkimmer @ppedrot