Skip to content

Actions: leanprover/lean4

Actions

All workflows

Actions

Loading...
Loading

Showing runs from all workflows
2,500+ workflow runs
2,500+ workflow runs

Filter by Workflow

⌥ + click/return to exclude

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
Kernel rejects structure J : Type (u+1) where x : Sort (imax (u+1) u) as "too big", though the elaborator accepts it Label PR based on Comment #32138: Issue comment #16242 (comment) created by nomeata
1s
1s
fix: respect debug.skipKernelTC when replaying realized constants Label PR based on Comment #32137: Issue comment #16243 (comment) created by nomeata
1s
1s
CI CI #66255: Scheduled
Queued master
master
Queued
feat: keep haves above a split match in equation lemmas Label PR based on Comment #32136: Issue comment #16235 (comment) created by leanprover-radar
1s
1s
feat: keep haves above a split match in equation lemmas Label PR based on Comment #32135: Issue comment #16235 (comment) created by leodemoura
7s
7s
PR release PR release #57722: completed by leodemoura
7m 19s
7m 19s
Grove Grove #29211: completed by leodemoura
42s
42s
feat: keep haves above a split match in equation lemmas Check for empty PR #9561: Pull request #16235 synchronize by leodemoura
1m 1s eqns-keep-have-match
eqns-keep-have-match
1m 1s
feat: keep haves above a split match in equation lemmas Check for modules that should use `prelude` #32322: Pull request #16235 synchronize by leodemoura
12s eqns-keep-have-match
eqns-keep-have-match
12s
feat: keep haves above a split match in equation lemmas CI #66254: Pull request #16235 synchronize by leodemoura
6m 35s eqns-keep-have-match
eqns-keep-have-match
6m 35s
feat: keep haves above a split match in equation lemmas Check for copyright header #32478: Pull request #16235 synchronize by leodemoura
1m 2s eqns-keep-have-match
eqns-keep-have-match
1m 2s
feat: keep haves above a split match in equation lemmas Check for stage0 changes #40305: Pull request #16235 synchronize by leodemoura
1m 4s eqns-keep-have-match
eqns-keep-have-match
1m 4s
feat: keep haves above a split match in equation lemmas Check PR title for commit convention #51867: Pull request #16235 synchronize by leodemoura
6s eqns-keep-have-match
eqns-keep-have-match
6s
feat: keep haves above a split match in equation lemmas Adaptation PR #7124: Pull request #16235 synchronize by leodemoura
27s
27s
feat: keep haves above a split match in equation lemmas Check PR body for changelog convention #54051: Pull request #16235 synchronize by leodemoura
8s
8s
feat: keep haves above a split match in equation lemmas Check stdlib_flags.h modifications #17060: Pull request #16235 synchronize by leodemoura
7s
7s
Universe approximation creates a cyclic level metavariable assignment and stack overflow Label PR based on Comment #32134: Issue comment #16125 (comment) created by user202729
1s
1s
feat: keep haves above a split match in equation lemmas Label PR based on Comment #32133: Issue comment #16235 (comment) created by downstream-lean4 Bot
15s
15s
feat: keep haves above a split match in equation lemmas Check stdlib_flags.h modifications #17059: Pull request #16235 labeled by leodemoura
8s
8s
feat: keep haves above a split match in equation lemmas Check PR body for changelog convention #54050: Pull request #16235 labeled by leodemoura
8s
8s
feat: keep haves above a split match in equation lemmas Adaptation PR #7123: Pull request #16235 labeled by leodemoura
49s
49s
feat: keep haves above a split match in equation lemmas Restart by label #13917: Pull request #16235 labeled by leodemoura
2s
2s
feat: keep haves above a split match in equation lemmas Backport #23859: Pull request #16235 labeled by leodemoura
1s
1s
PR release PR release #57721: completed by leodemoura
11m 20s
11m 20s
Grove Grove #29210: completed by leodemoura
32s
32s