leanprover-community-mathlib4-bot

Results 107 comments of leanprover-community-mathlib4-bot

feat: use `rfl` proofs of `Iff` in `dsimp`

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ❌ Mathlib branch [lean-pr-testing-3973](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-3973) built against this PR, but linting failed. (2024-04-23 01:08:08) [View Log](https://github.com/leanprover-community/mathlib4/actions/runs/8793038884) - ❌ Mathlib branch [lean-pr-testing-3973](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-3973) built against this PR, but...

refactor: lake: manifest semver & code cleanup

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ✅ Mathlib branch [lean-pr-testing-4083](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4083) has successfully built against this PR. (2024-05-06 23:29:54) [View Log](https://github.com/leanprover-community/mathlib4/actions/runs/8976532337) - ✅ Mathlib branch [lean-pr-testing-4083](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4083) has successfully built against this PR....

fix: validate UTF-8 at C++ -> Lean boundary

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ❗ Std/Mathlib CI will not be attempted unless your PR branches off the `nightly-with-mathlib` branch. Try `git rebase 62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a --onto 291bb84c972dae470e8f5602729e9d5a5e9433a2`. (2024-04-20 20:29:09) - ❗...

feat: support Lake for building Lean core oleans

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ❗ Std/Mathlib CI will not be attempted unless your PR branches off the `nightly-with-mathlib` branch. Try `git rebase 092ca8530a6f272b7cb19235750479cdffab11de --onto b470eb522bfd68ca96938c23f6a1bce79da8a99f`. (2024-05-03 08:38:43) - ❗...

experiment: split PHashMap / PHashMapSized

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

doc: `lean.h`

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

feat: do not propagate pretty printer errors through messages

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ❗ Std/Mathlib CI will not be attempted unless your PR branches off the `nightly-with-mathlib` branch. Try `git rebase 0b01ceb3bb3334fd6c2f3b24996646046722c62a --onto 0ec8862103e397715854a7a6962ce542bba4884d`. (2024-03-16 20:03:01) - ❌...