leanprover-community-bot comments

Results 17 comments of


                                            leanprover-community-bot

trafficstars

perf: add a bitblasting cache for bv_decide's boolean substructure

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-2025-04-21` tag does not exist there yet. We will retry when you push more commits....

refactor: migrate all usages of old slice notation

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-2025-06-24` tag does not exist there yet. We will retry when you push more commits....

fix: init git only not inside git work tree

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-10-21` tag does not exist there yet. We will retry when you push more commits....

fix: wildcard `generalize` only generalizes visible theorems

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ✅ Mathlib branch [lean-pr-testing-4846](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-4846) has successfully built against this PR. (2024-10-25 02:40:40) [View Log](https://github.com/leanprover-community/mathlib4/actions/runs/11510486930)

feat: add `#print opaques` command

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ✅ Mathlib branch [batteries-pr-testing-966](https://github.com/leanprover-community/mathlib4/compare/master...batteries-pr-testing-966) has successfully built against this PR. (2024-09-27 13:04:22) [View Log](https://github.com/leanprover-community/mathlib4/actions/runs/11070236811) - ✅ Mathlib branch [batteries-pr-testing-966](https://github.com/leanprover-community/mathlib4/compare/master...batteries-pr-testing-966) has successfully built against this PR....

refactor: construc `.eq_def` before `.eq_n`

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - 💥 Mathlib branch [lean-pr-testing-5669](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-5669) build failed against this PR. (2024-10-10 17:18:37) [View Log](https://github.com/leanprover-community/mathlib4/actions/runs/11278799550) - 💥 Mathlib branch [lean-pr-testing-5669](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-5669) build failed against this PR. (2024-10-10 20:58:55)...

chore: add LNSym omega benchmarks with large problems that take multiple seconds to solve

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 5dea30f169b91cdda9a3903a7a9d125e0f075605 --onto a4fda010f3d44c02393d5afd5cf05509989daf63`. (2024-10-04 20:01:17) - ❗...