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

[Merged by Bors] - fix: make convert tactic use convert suffix for goals from anonymous placeholders #3314

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - fix: make convert tactic use convert suffix for goals from anonymous placeholders #3314

wants to merge 1 commit into from

Conversation

alexjbest
Copy link
Member

@alexjbest alexjbest commented Apr 6, 2023 •
edited by kmill
Loading

The convert tactic mistakenly calls elabTermWithHoles using the main goal's tag for the suffix. For example, if the main goal tag was inl this would produce tags like inl.inl_1 for goals associated to anonymous placeholders. We change convert to use the suffix convert instead, yielding subgoals like inl.convert_1 for these.

The previous behavior caused a panic in #3312 due to macro scopes in goal tags, which this fix happily sidesteps.

Open in Gitpod

@alexjbest alexjbest requested a review from digama0 April 6, 2023 18:33
@alexjbest alexjbest added awaiting-review t-meta Tactics, attributes or user commands labels Apr 6, 2023
@kmill
Copy link
Contributor

kmill commented Apr 6, 2023

I'm not sure this is the right fix; I believe the bug is in tagUntaggedGoals. Here's a previous fix for a similar issue: leanprover/lean4@d5fb32a

(Zulip thread)

@alexjbest
Copy link
Member Author

alexjbest commented Apr 6, 2023 •
edited
Loading

I agree changing that would also be (possibly) a good idea.
But I do think the blah.blah_1 behavior is undesirable and dodging the append issue is a (nice) side effect of this change that doesn't involve fixing core.

@Parcly-Taxel Parcly-Taxel mentioned this pull request Apr 9, 2023
Closed
@kmill kmill changed the title chore: make convert name new goals with convert fix: make convert tactic use convert suffix for new goals from anonymous placeholders Apr 13, 2023
@kmill kmill changed the title fix: make convert tactic use convert suffix for new goals from anonymous placeholders fix: make convert tactic use convert suffix for goals from anonymous placeholders Apr 13, 2023
@kmill
Copy link
Contributor

kmill commented Apr 13, 2023

Ah, I was misreading the source code and thought getMainTag was being passed to mkFreshExprMVar. This is definitely the right thing to do, thanks!

bors r+

It looks like the trans tactic has the same bug.

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 13, 2023
bors bot pushed a commit that referenced this pull request Apr 13, 2023
@alexjbest
fix: make convert tactic use convert suffix for goals from anonymou…
a4d9db8 
…s placeholders (#3314)

The `convert` tactic mistakenly calls `elabTermWithHoles` using the main goal's tag for the suffix. For example, if the main goal tag was `inl` this would produce tags like `inl.inl_1` for goals associated to anonymous placeholders. We change convert to use the suffix `convert` instead, yielding subgoals like `inl.convert_1` for these.

The previous behavior caused a panic in #3312 due to macro scopes in goal tags, which this fix happily sidesteps.
@alexjbest
Copy link
Member Author

@kmill yes I think so too, but when I tried I couldn't actually produce an example where I saw bad behaviour, so I left changing that out of this pr.

@bors
Copy link

bors bot commented Apr 13, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title fix: make convert tactic use convert suffix for goals from anonymous placeholders [Merged by Bors] - fix: make convert tactic use convert suffix for goals from anonymous placeholders Apr 13, 2023
@bors bors bot closed this Apr 13, 2023
@bors bors bot deleted the alexjbest/name_convert branch April 13, 2023 16:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 Awaiting requested review from digama0

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@alexjbest @kmill