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.

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

feat: resolve generalized field notation using all parents #5770

Merged
merged 1 commit into from
Oct 31, 2024

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Oct 19, 2024

  • Now getPathToBaseStructure? can navigate to all parent structures, not just through subobjects.
  • Adds a "resolution order" for methods. This is the order that generalized field notation visits parent structures when trying to resolve names. The algorithm to compute a resolution order is the commonly used C3 (used for instance by Python). By default we use a relaxed version of the algorithm that tolerates inconsistencies. Using set_option structure.strictResolutionOrder true makes inconsistent parent orderings into warnings.
  • This makes generalized field notation be able to resolve names for all parent structures, not just those that are embedded as subobjects. Closes Dot notation resolution has counterintuitive behavior with diamond multiple inheritance  #3467. (And addresses side note in [RFC] record all parents structures in StructureInfo #1881.)
  • Modifies getAllParentStructures to return all parents. This improves dot completion in the editor.

@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 19, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 19, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 19, 2024
@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 19, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 19, 2024

Mathlib CI status (docs):

  • 💥 Mathlib branch lean-pr-testing-5770 build failed against this PR. (2024-10-19 09:33:13) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4ee44ceb1d77f16b9b81bc655bc8b318cd6e8c4d --onto 9847923f9be5de968f10ed7c7493e3ca0072abce. (2024-10-29 02:24:06)
  • 💥 Mathlib branch lean-pr-testing-5770 build failed against this PR. (2024-10-30 01:00:19) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0fcee100e7ea382069854d91e854265c56b54428 --onto 38c39482f40536b864a9b43c718e10e8413b26e5. (2024-10-31 07:25:48)
  • ✅ Mathlib branch lean-pr-testing-5770 has successfully built against this PR. (2024-10-31 16:41:18) View Log

kmill added a commit to leanprover-community/aesop that referenced this pull request Oct 19, 2024
MonadStats was extending `MonadLiftT` twice, but the two parents were defeq. This was a hack to get around the fact that the parent instances were providing `MonadLiftT` instances rather than a `MonadLift` instance, breaking `MonadLiftT` inference.

This changes it to *not* extend `MonadLiftT`, instead embedding it as a field, and then writing an explicit `MonadLift` instance.

This is motivated by [lean4#5770](leanprover/lean4#5770), which will log warnings when structures extend parents multiple times.
src/Lean/Structure.lean Outdated Show resolved Hide resolved
src/Lean/Structure.lean Outdated Show resolved Hide resolved
@kmill kmill force-pushed the structure_mro branch 2 times, most recently from 0f9b6cf to 1229fd7 Compare October 29, 2024 02:47
@kmill kmill marked this pull request as ready for review October 29, 2024 02:57
@kmill kmill requested a review from mhuisi as a code owner October 29, 2024 02:57
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 30, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 30, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 31, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 31, 2024
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Oct 31, 2024
@kmill kmill enabled auto-merge October 31, 2024 21:04
@kmill kmill added this pull request to the merge queue Oct 31, 2024
Merged via the queue into leanprover:master with commit 465ed8a Oct 31, 2024
18 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Dot notation resolution has counterintuitive behavior with diamond multiple inheritance
3 participants