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

fix: use Name.appendCore instead of Name.append in unresolveNameGlobal #3946

Merged
merged 2 commits into from
Apr 24, 2024
Merged

fix: use Name.appendCore instead of Name.append in unresolveNameGlobal #3946

merged 2 commits into from
Apr 24, 2024

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Apr 19, 2024 •
edited
Loading

Name.append has special handling of macro scopes, and it would cause unresolveNameGlobal to panic. Using Name.appendCore to append name parts is justified by the fact that it's being used to reassemble a disassembled name.

Closes #2291

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 19, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Apr 19, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b6d77be6a5ced7cbd7b6e051047158e7e07bee4e --onto d3e004932c1f5ac3946850692940512d381c7634. (2024-04-19 01:08:22)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b6d77be6a5ced7cbd7b6e051047158e7e07bee4e --onto 62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a. (2024-04-22 01:47:31)

@kmill kmill added the awaiting-review Waiting for someone to review the PR label Apr 22, 2024
@kim-em
Copy link
Collaborator

kim-em commented Apr 22, 2024

Do we need some sort of warning note on Name.append? If not, LGTM.

@kmill
Copy link
Collaborator Author

kmill commented Apr 22, 2024

@semorrison It turns out the docstring wasn't accurate, so it was worth modifying it anyway.

kmill added 2 commits April 24, 2024 07:26
@kmill
fix: use Name.appendCore instead of Name.append in `unresolveName…
ff2ef25 
…Global`

`Name.append` has special handling of macro scopes, and it would cause `unresolveNameGlobal` to panic.

Closes leanprover#2291
@kmill
update docstring for Lean.Name.Append
80e9292
@kmill kmill added this pull request to the merge queue Apr 24, 2024
Merged via the queue into leanprover:master with commit a9db0d2 Apr 24, 2024
10 checks passed
@kmill kmill mentioned this pull request May 7, 2024
Merged
github-merge-queue bot pushed a commit that referenced this pull request May 10, 2024
@kmill
chore: tidying up Lean.unresolveNameGlobal (#4091)
a1be9ec 
The main loop logic could be simplified, and `if let` could be used to
make control flow more obvious.

Also adds a check for macro scopes to prevent `unresolveNameGlobal` from
returning names with macro scopes in the event there's an alias with
one.

This is a follow up to #3946.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em approved these changes

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

panic in delabConst when trace.compiler is enabled
3 participants
@kmill @leanprover-community-mathlib4-bot @kim-em