Skip to content

Actions: leanprover/lean4

Actions

Backport

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
backport.yml
2,500+ workflow runs
2,500+ workflow runs

Filter by Event

⌥ + click/return to exclude

Filter by Status

⌥ + click/return to exclude

Filter by Branch

⌥ + click/return to exclude

Filter by Actor

⌥ + click/return to exclude
feat: allow a general evalTac at evalSepTactics Backport #22116: Pull request #7702 closed by kim-em
In progress
In progress
fix: simp? output order Backport #22115: Pull request #9117 closed by kim-em
1s
1s
feat: Constructions for splitting and merging vectors of bitvectors Backport #22114: Pull request #7754 closed by kim-em
1s
1s
chore: permit Lake failures in PR release CI Backport #22113: Pull request #6403 closed by kim-em
11s
11s
feat: change_matching ... with tactic Backport #22112: Pull request #6018 closed by kim-em
1s
1s
feat: qsort with proven bounds and correctness proof Backport #22111: Pull request #5346 closed by kim-em
1s
1s
chore: rename 13 simp lemmas Backport #22110: Pull request #5317 closed by kim-em
7s
7s
feat: binary recursive implementation of List.mapA Backport #22109: Pull request #3877 closed by kim-em
1s
1s
feat: set_option for conv mode Backport #22108: Pull request #2887 closed by kim-em
1s
1s
feat: opaque_repr attribute to suppress "trivial structure" opt Backport #22107: Pull request #2292 closed by kim-em
1s
1s
Use Bool.asProp for coercions Backport #22106: Pull request #2060 closed by kim-em
1s
1s
feat: show tactic (full version) Backport #22105: Pull request #1749 closed by kim-em
1s
1s
perf: cache elaboration of section variables across commands Backport #22104: Pull request #14595 closed by marcelolynch
1s
1s
fix: use the correct calling convention when over-applying a closure in lean_apply_m Backport #22103: Pull request #14969 closed by Kha
6s
6s
feat: lake: separate leanir job Backport #22102: Pull request #14906 labeled by mathlib-lean-pr-testing Bot
6s
6s
fix: use the correct calling convention when over-applying a closure in lean_apply_m Backport #22101: Pull request #14969 labeled by Kha
1s
1s
perf: fuse heartbeat update into the small-object allocation call Backport #22100: Pull request #14981 labeled by mathlib-lean-pr-testing Bot
1s
1s
perf: heartbeat and theap in one thread-local Backport #22099: Pull request #14982 labeled by mathlib-lean-pr-testing Bot
1s
1s
perf: derive array capacity from mi_usable_size Backport #22098: Pull request #14979 labeled by mathlib-lean-pr-testing Bot
7s
7s
perf: do not include scalar children in mark_mt/mark_persistent Backport #22097: Pull request #14980 labeled by mathlib-lean-pr-testing Bot
1s
1s
perf: avoid copying mpz wrappers Backport #22096: Pull request #14978 labeled by mathlib-lean-pr-testing Bot
1s
1s
perf: avoid copying mpz wrappers Backport #22095: Pull request #14978 closed by TwoFX
10s
10s
just for bench Backport #22094: Pull request #14976 closed by TwoFX
1s
1s
perf: avoid setTransparency when the transparency is already in effect Backport #22093: Pull request #14967 closed by Kha
10s
10s
feat: characterize when T-division equals zero Backport #22092: Pull request #8204 closed by kim-em
7s
7s