leanprover-community-mathlib4-bot comments

Results 107 comments of


                                            leanprover-community-mathlib4-bot

fix: take `synthPendingDepth` into account when caching TC results

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - 💥 Mathlib branch [lean-pr-testing-4120](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4120) build failed against this PR. (2024-05-10 01:25:46) [View Log](https://github.com/leanprover-community/mathlib4/actions/runs/9025556143) - 💥 Mathlib branch [lean-pr-testing-4120](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4120) build failed against this PR. (2024-05-10 02:14:10)...

fix: type class issues

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - 💥 Mathlib branch [lean-pr-testing-4114](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4114) build failed against this PR. (2024-05-09 01:32:33) [View Log](https://github.com/leanprover-community/mathlib4/actions/runs/9010578573) - 💥 Mathlib branch [lean-pr-testing-4114](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4114) build failed against this PR. (2024-05-09 02:27:02)...

fix: check that funind-reserved names are available

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ✅ Mathlib branch [lean-pr-testing-4135](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4135) has successfully built against this PR. (2024-05-11 12:55:17) [View Log](https://github.com/leanprover-community/mathlib4/actions/runs/9043402275) - ✅ Mathlib branch [lean-pr-testing-4135](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4135) has successfully built against this PR....

chore: add warning comments about `findM?`

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the `nightly-with-mathlib` branch. Try `git rebase ca6437df717b550cbea3e110f3093c1250d5c5be --onto fe7b96d8a0cf85e1ea81791ac9d673f84c9e866d`. (2024-05-10 07:09:17)

feat: make frontend normalize line endings to LF

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ❗ Std CI can not be attempted yet, as the `nightly-testing-2024-05-07` tag does not exist there yet. We will retry when you push more commits....

refactor: lake: import errors, job captions, log grouping

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - 🟡 Mathlib branch [lean-pr-testing-4115](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4115) build this PR didn't complete normally. (2024-05-09 03:08:51) [View Log](https://github.com/leanprover-community/mathlib4/actions/runs/9011764266) - ✅ Mathlib branch [lean-pr-testing-4115](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4115) has successfully built against this PR....

feat: make `registerLabelAttr` consistent with `registerTagAttribute`

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - 💥 Mathlib branch [lean-pr-testing-3699](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-3699) build failed against this PR. (2024-03-16 22:12:04) [View Log](https://github.com/leanprover-community/mathlib4/actions/runs/8310727893) - 💥 Mathlib branch [lean-pr-testing-3699](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-3699) build failed against this PR. (2024-03-16 22:32:05)...

fix: hovers on binders with metavariables

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ✅ Mathlib branch [lean-pr-testing-4137](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4137) has successfully built against this PR. (2024-05-11 17:47:57) [View Log](https://github.com/leanprover-community/mathlib4/actions/runs/9045077779) - ✅ Mathlib branch [lean-pr-testing-4137](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4137) has successfully built against this PR....

chore: rerun CI only when full-ci label is added or removed

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ❗ Batteries CI can not be attempted yet, as the `nightly-testing-2024-05-11` tag does not exist there yet. We will retry when you push more commits....

fix: type class issues with `maxSynthPendingDepth := 1`

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - 💥 Mathlib branch [lean-pr-testing-4119](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4119) build failed against this PR. (2024-05-10 01:22:48) [View Log](https://github.com/leanprover-community/mathlib4/actions/runs/9025554873) - 💥 Mathlib branch [lean-pr-testing-4119](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4119) build failed against this PR. (2024-05-10 02:02:52)...