[Merged by Bors] - feat: miscellaneous improvements to the differential geometry elaborators by grunweg · Pull Request #28032 · leanprover-community/mathlib4

grunweg · 2025-08-06T09:59:29Z

Support inferring the model with corners on a TangentBundle.
Support inferring the model with corners on the space H a manifold is modelled on.
Correct the grammar in an error message.
Extend the tracing to show a bit more information.
Use backticks in all tracing (and other) error messages, per zulip discussion
Add some more tests, including one which is currently failing.

depends on: [Merged by Bors] - feat: support coercions in the differential geometry elaborators #30307

github-actions · 2025-08-06T10:00:52Z

PR summary 6e58d23346

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

leanprover-community#28032 adds a test for this; no need to track it here

…rover-community#28032

thorimur

Looks good! I'm excited to get these elaborator improvements in at a steady pace! :D (I'd like to give it a once-over after #30307 lands just to make sure the diff is reasonable.)

Mathlib/Geometry/Manifold/Notation.lean

grunweg · 2025-10-10T00:25:56Z

Thanks; I agree with both your comments. I'll ping you once the dependent PR has been merged.

grunweg · 2025-10-10T04:05:22Z

I rebased on top of #30307, and uplifted a few tweaks from #30357. Each commit is (hopefully) self-contained.

grunweg · 2025-10-10T04:46:26Z

I have two more small features in the pipeline, in #30357 (inferring the model with corners on a charted space, and on a space of continuous linear maps). Would you prefer me folding that into this PR, or rather a follow-up?

grunweg · 2025-10-10T16:02:54Z

Actually: let me fold the charted space one into this PR, and leave the other one to a follow-up (together with a few more such changes).

Mathlib/Geometry/Manifold/Notation.lean

thorimur · 2025-10-10T18:05:57Z

(Once again these changes look good, pending a once-over after the blocking PR lands! :) )

mathlib4-dependent-issues-bot · 2025-10-14T15:24:53Z

This PR/issue depends on:

~~[Merged by Bors] - feat: support coercions in the differential geometry elaborators #30307~~
By Dependent Issues (🤖). Happy coding!

mathlib4-merge-conflict-bot · 2025-10-14T16:33:48Z

This pull request has conflicts, please merge master and resolve them.

Mathlib/Geometry/Manifold/Notation.lean

Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

Mathlib/Geometry/Manifold/Notation.lean

thorimur · 2025-10-15T00:11:25Z

Wonderful, LGTM! :) 🎉

Vierkantor

The meta code looks fine to me, and this looks really well tested! But this really is not my area of expertise, mathematics-wise, so I really cannot say if the tests cover the functionality well. Could a differential geometer confirm that this makes sense?

maintainer merge

github-actions · 2025-10-15T12:29:16Z

🚀 Pull request has been placed on the maintainer queue by Vierkantor.

fpvandoorn · 2025-10-15T12:33:17Z

LGTM

bors merge

…tors (#28032) - Support inferring the model with corners on a `TangentBundle`. - Support inferring the model with corners on the space `H` a manifold is modelled on. - Correct the grammar in an error message. - Extend the tracing to show a bit more information. - Use backticks in all tracing (and other) error messages, per [zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Style.3A.20Backticks.20in.20messages.3F/with/544859886) - Add some more tests, including one which is currently failing. Co-authored-by: thorimur <thomasmurrills@gmail.com> Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

mathlib-bors · 2025-10-15T13:28:16Z

Pull request successfully merged into master.

Build succeeded:

…tors (leanprover-community#28032) - Support inferring the model with corners on a `TangentBundle`. - Support inferring the model with corners on the space `H` a manifold is modelled on. - Correct the grammar in an error message. - Extend the tracing to show a bit more information. - Use backticks in all tracing (and other) error messages, per [zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Style.3A.20Backticks.20in.20messages.3F/with/544859886) - Add some more tests, including one which is currently failing. Co-authored-by: thorimur <thomasmurrills@gmail.com> Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

github-actions bot added the t-differential-geometry Manifolds etc label Aug 6, 2025

grunweg mentioned this pull request Oct 7, 2025

[Merged by Bors] - feat: support coercions in the differential geometry elaborators #30307

Closed

1 task

grunweg force-pushed the diffgeo-custom-elaborators-charts branch from 09fb0bd to 93ea5fa Compare October 8, 2025 19:53

grunweg changed the title ~~feat: support Partial{Homeomorph,Equiv} in differential geometry elaborators~~ feat: miscellaneous improvements to the differential geometry elaborators Oct 8, 2025

grunweg added the t-meta Tactics, attributes or user commands label Oct 8, 2025

grunweg force-pushed the diffgeo-custom-elaborators-charts branch from 93ea5fa to 77636ac Compare October 8, 2025 20:22

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 8, 2025

grunweg added a commit to grunweg/mathlib4 that referenced this pull request Oct 8, 2025

chore: remove TODO comments

7152199

leanprover-community#28032 adds a test for this; no need to track it here

grunweg added a commit to grunweg/mathlib4 that referenced this pull request Oct 8, 2025

chore: forward-port changes from leanprover-community#30307 and leanp…

bf8dcd0

…rover-community#28032

grunweg mentioned this pull request Oct 9, 2025

chore: golf using custom elaborators #30357

Closed

1 task

thorimur reviewed Oct 9, 2025

View reviewed changes

Mathlib/Geometry/Manifold/Notation.lean Outdated Show resolved Hide resolved

Mathlib/Geometry/Manifold/Notation.lean Show resolved Hide resolved

grunweg force-pushed the diffgeo-custom-elaborators-charts branch from 199abc8 to 2c74842 Compare October 10, 2025 03:56

grunweg mentioned this pull request Oct 10, 2025

[Merged by Bors] - chore: split test file for differential geometry elaborators #30412

Closed

1 task

thorimur reviewed Oct 10, 2025

View reviewed changes

Mathlib/Geometry/Manifold/Notation.lean Outdated Show resolved Hide resolved

grunweg mentioned this pull request Oct 13, 2025

Tracking issue for differential geometry elaborators #30503

Open

26 tasks

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 14, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 14, 2025

grunweg force-pushed the diffgeo-custom-elaborators-charts branch from 364ff67 to 03bc6e7 Compare October 14, 2025 18:01

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 14, 2025

grunweg force-pushed the diffgeo-custom-elaborators-charts branch from 640b9a6 to 7965974 Compare October 14, 2025 18:12

grunweg added 2 commits October 14, 2025 20:14

chore: move tests to a better place

85fa105

More tests

76a2689

Two last tests for partial homeomorphisms and equivalences.

d65dc91

grunweg force-pushed the diffgeo-custom-elaborators-charts branch from b46de46 to d65dc91 Compare October 14, 2025 18:15

thorimur reviewed Oct 14, 2025

View reviewed changes

Mathlib/Geometry/Manifold/Notation.lean Outdated Show resolved Hide resolved

grunweg and others added 3 commits October 14, 2025 22:24

Update Mathlib/Geometry/Manifold/Notation.lean

0277991

Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

Update

15c5420

Better tracing for charted space search

6266d04

thorimur reviewed Oct 14, 2025

View reviewed changes

Mathlib/Geometry/Manifold/Notation.lean Outdated Show resolved Hide resolved

Tweak other tracing in the same way

84531fd

thorimur reviewed Oct 14, 2025

View reviewed changes

Mathlib/Geometry/Manifold/Notation.lean Outdated Show resolved Hide resolved

grunweg and others added 2 commits October 14, 2025 22:52

Fix typo

46a7eba

chore: apply suggestion

2427807

thorimur reviewed Oct 14, 2025

View reviewed changes

Mathlib/Geometry/Manifold/Notation.lean Outdated Show resolved Hide resolved

Tweak one message, move another

f2c7805

chore: put backticks around expressions consistently

90e5c92

grunweg requested a review from Vierkantor October 15, 2025 10:15

Vierkantor self-assigned this Oct 15, 2025

Vierkantor approved these changes Oct 15, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 15, 2025

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Oct 15, 2025

mathlib-bors bot changed the title ~~feat: miscellaneous improvements to the differential geometry elaborators~~ [Merged by Bors] - feat: miscellaneous improvements to the differential geometry elaborators Oct 15, 2025

mathlib-bors bot closed this Oct 15, 2025

grunweg deleted the diffgeo-custom-elaborators-charts branch October 15, 2025 13:30

Conversation

grunweg commented Aug 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Aug 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 6e58d23346

Import changes for modified files

Declarations diff

Uh oh!

thorimur left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

grunweg commented Oct 10, 2025

Uh oh!

grunweg commented Oct 10, 2025

Uh oh!

grunweg commented Oct 10, 2025

Uh oh!

grunweg commented Oct 10, 2025

Uh oh!

Uh oh!

thorimur commented Oct 10, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Oct 14, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Oct 14, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thorimur commented Oct 15, 2025

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Oct 15, 2025

Uh oh!

fpvandoorn commented Oct 15, 2025

Uh oh!

mathlib-bors bot commented Oct 15, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

grunweg commented Aug 6, 2025 •

edited

Loading

github-actions bot commented Aug 6, 2025 •

edited

Loading