Skip to content

Actions: leanprover/lean4

Actions

Adaptation PR

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
adaptation-pr.yml
432 workflow runs
432 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
fix: enforce set notation per-element indentation Adaptation PR #432: Pull request #14350 labeled by leanprover-bot
1s
1s
test: fsanitize exclusion cleanup Adaptation PR #431: Pull request #14349 closed by Kha
45s
45s
experiment: consolidate all TC opts Adaptation PR #430: Pull request #14339 labeled by mathlib-lean-pr-testing Bot
1s
1s
test: fsanitize exclusion cleanup Adaptation PR #429: Pull request #14349 labeled by Kha
1s
1s
perf: use WHNF cache in whnfMatcher also at sub-default transparency Adaptation PR #428: Pull request #14323 ready_for_review by datokrat
47s
47s
perf: use WHNF cache in whnfMatcher also at sub-default transparency Adaptation PR #427: Pull request #14323 labeled by leanprover-bot
Skipped
Skipped
chore: revert "chore: cmake: disable Lake cache on PREV_STAGE use as well" Adaptation PR #426: Pull request #14347 closed by Kha
48s
48s
test: add vcgen benchmark over the verina corpus Adaptation PR #425: Pull request #14340 closed by sgraf812
35s
35s
doc: fix incorrect examples of K-like reduction in RecursorVal docstring Adaptation PR #424: Pull request #13967 closed by kmill
39s
39s
fix: load missing dynlibs individually with precompileModules Adaptation PR #423: Pull request #14326 labeled by mathlib-lean-pr-testing Bot
1s
1s
fix: load missing dynlibs individually with precompileModules Adaptation PR #422: Pull request #14326 labeled by Vtec234
1s
1s
fix: load missing dynlibs individually with precompileModules Adaptation PR #421: Pull request #14326 labeled by leanprover-bot
8s
8s
perf: construct IntModule.OfNatModule.Q type manually Adaptation PR #420: Pull request #14346 labeled by mathlib-lean-pr-testing Bot
1s
1s
perf: construct IntModule.OfNatModule.Q type manually Adaptation PR #419: Pull request #14346 closed by leodemoura
1m 4s
1m 4s
perf: construct IntModule.OfNatModule.Q type manually Adaptation PR #418: Pull request #14346 labeled by leanprover-bot
1s
1s
perf: construct IntModule.OfNatModule.Q type manually Adaptation PR #417: Pull request #14346 labeled by leodemoura
1s
1s
chore: repeat some benchmarks to avoid outliers Adaptation PR #416: Pull request #14342 closed by Garmelon
39s
39s
refactor: split registerParametricAttribute into extension creation and registration Adaptation PR #415: Pull request #14344 labeled by mathlib-lean-pr-testing Bot
1s
1s
chore: repeat some benchmarks to avoid outliers Adaptation PR #414: Pull request #14342 labeled by mathlib-lean-pr-testing Bot
1s
1s
refactor: split registerParametricAttribute into extension creation and registration Adaptation PR #413: Pull request #14344 labeled by leanprover-bot
1s
1s
perf: cache intermediate type class results and non-results Adaptation PR #412: Pull request #4272 closed by JovanGerb
37s
37s
chore: use ' instead of brackets for quotes Adaptation PR #411: Pull request #4464 closed by JovanGerb
37s
37s
experiment: consolidate all TC opts Adaptation PR #410: Pull request #14339 labeled by mathlib-lean-pr-testing Bot
7s
7s
fix: run shell main on a thread with the configured stack size Adaptation PR #409: Pull request #14343 closed by Kha
43s
43s
refactor: split registerParametricAttribute into extension creation and registration Adaptation PR #408: Pull request #14344 labeled by wkrozowski
1s
1s