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: include references in attributes in call hierarchy #5650

Merged
merged 5 commits into from
Oct 18, 2024
Merged

fix: include references in attributes in call hierarchy #5650

merged 5 commits into from
Oct 18, 2024

Conversation

Kha
Copy link
Member

@Kha Kha commented Oct 8, 2024

By ensuring all declModifiers are included in addDeclarationRanges, implementedBy references etc are included in the call hierarchy

@Kha Kha requested a review from mhuisi October 8, 2024 08:39
@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 Oct 8, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 8, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5650
774f500
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 8, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5650
3d635a4
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Oct 8, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 8, 2024 •
edited
Loading

Mathlib CI status (docs):

  • 💥 Mathlib branch lean-pr-testing-5650 build failed against this PR. (2024-10-08 09:03:34) View Log
  • 💥 Mathlib branch lean-pr-testing-5650 build failed against this PR. (2024-10-08 10:05:02) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a167860e3b2a1236af3e989259f5badc04d50b8c --onto 3a34a8e0d119d8a907614af62b405d85149672f0. (2024-10-18 15:42:18)

@Kha Kha requested a review from digama0 as a code owner October 8, 2024 09:42
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 8, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5650
40e75b7
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 8, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5650
f28771c
@Kha Kha enabled auto-merge October 18, 2024 12:23
@Kha Kha added this pull request to the merge queue Oct 18, 2024
Merged via the queue into leanprover:master with commit 11ae8ba Oct 18, 2024
13 checks passed
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 19, 2024
@kim-em
fixes for leanprover/lean4#5650
c2067f2
@Kha Kha deleted the push-lxvtzpmvwskk branch October 21, 2024 09:02
@Kha Kha mentioned this pull request Oct 21, 2024
Merged
Kha added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 22, 2024
@Kha
Revert "fixes for leanprover/lean4#5650"
d768d29 
This reverts commit c2067f2.
github-merge-queue bot pushed a commit that referenced this pull request Oct 23, 2024
@Kha
refactor: nicer modifiers/ranges API (#5788)
174a5f3 
Cleanup of #5650 

* default `Modifiers.stx` to missing
* rename and clarify `addDeclarationRangesFromSyntax` as the main
convenience function for user metaprograms
tobiasgrosser pushed a commit to opencompl/lean4 that referenced this pull request Oct 27, 2024
@Kha @tobiasgrosser
refactor: nicer modifiers/ranges API (leanprover#5788)
35efb1a 
Cleanup of leanprover#5650 

* default `Modifiers.stx` to missing
* rename and clarify `addDeclarationRangesFromSyntax` as the main
convenience function for user metaprograms
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mhuisi mhuisi Awaiting requested review from mhuisi

@digama0 digama0 Awaiting requested review from digama0 digama0 is a code owner

Assignees
No one assigned
Labels
breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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.
2 participants
@Kha @leanprover-community-bot