Skip to content

Actions: leanprover/lean4

Actions

CI

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
ci.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: intrinsic verification syntax for do-notation loops and def contracts CI #60704: Pull request #14389 synchronize by sgraf812
In progress sg/kr1-intrinsic-do
sg/kr1-intrinsic-do
In progress
fix: better defeq error messages CI #60703: Pull request #14537 synchronize by datokrat
In progress datokrat:defeq-errors
datokrat:defeq-errors
In progress
CI CI #60702: Merge group checks requested
In progress
In progress
perf: pick compacted-region base addresses outside ASLR-occupied zones CI #60701: Pull request #14563 opened by sgraf812
13m 2s sg/olean-base-window
sg/olean-base-window
13m 2s
feat: support code actions in linters (#14402) CI #60700: Commit 76e5ec5 pushed by github-merge-queue Bot
33m 3s master
master
33m 3s
refactor: split registerParametricAttribute into extension creation… CI #60699: Commit 8db1810 pushed by github-merge-queue Bot
29m 11s master
master
29m 11s
CI CI #60698: Merge group checks requested
41m 49s
41m 49s
perf: compare forbiddenTks by pointer first in parser cache keys CI #60697: Pull request #14562 opened by sgraf812
16m 41s sg/parser-cache-ptr-beq
sg/parser-cache-ptr-beq
16m 41s
CI CI #60696: Merge group checks requested
33m 49s
33m 49s
CI CI #60695: Scheduled
1h 40m 0s master
master
1h 40m 0s
feat: intrinsic verification syntax for do-notation loops and def contracts CI #60694: Pull request #14389 synchronize by sgraf812
17m 2s sg/kr1-intrinsic-do
sg/kr1-intrinsic-do
17m 2s
feat: expand byte array api CI #60693: Pull request #8165 synchronize by Rob23oba
20s Rob23oba:byte-array-additions
Rob23oba:byte-array-additions
20s
feat: Decidable as subtype of Bool CI #60692: Pull request #8309 synchronize by Rob23oba
1h 10m 47s Rob23oba:decidable-as-bool
Rob23oba:decidable-as-bool
1h 10m 47s
feat: Decidable as subtype of Bool CI #60691: Pull request #8309 synchronize by Rob23oba
4m 17s Rob23oba:decidable-as-bool
Rob23oba:decidable-as-bool
4m 17s
feat: Decidable as subtype of Bool CI #60690: Pull request #8309 synchronize by Rob23oba
35m 39s Rob23oba:decidable-as-bool
Rob23oba:decidable-as-bool
35m 39s
feat: Decidable as subtype of Bool CI #60689: Pull request #8309 synchronize by Rob23oba
14m 23s Rob23oba:decidable-as-bool
Rob23oba:decidable-as-bool
14m 23s
feat: Decidable as subtype of Bool CI #60688: Pull request #8309 synchronize by Rob23oba
21m 26s Rob23oba:decidable-as-bool
Rob23oba:decidable-as-bool
21m 26s
feat: Decidable as subtype of Bool CI #60687: Pull request #8309 synchronize by Rob23oba
4m 38s Rob23oba:decidable-as-bool
Rob23oba:decidable-as-bool
4m 38s
feat: Decidable as subtype of Bool CI #60686: Pull request #8309 synchronize by Rob23oba
1h 15m 38s Rob23oba:decidable-as-bool
Rob23oba:decidable-as-bool
1h 15m 38s
perf: normalize free variables in the type class resolution cache key CI #60685: Pull request #14369 synchronize by Kha
10m 10s push-umqqwtmwmmyx
push-umqqwtmwmmyx
10m 10s
perf: normalize free variables in the type class resolution cache key CI #60684: Pull request #14369 synchronize by Kha
7m 34s push-umqqwtmwmmyx
push-umqqwtmwmmyx
7m 34s
fix: ensure lean_initialize is called when Lean is only privately… CI #60683: Commit 0bfc3ac pushed by github-merge-queue Bot
34m 59s master
master
34m 59s
fix: preserve expected types of nested proofs CI #60682: Pull request #14557 synchronize by kernelpanic888
14m 40s kernelpanic888:codex/simp-hoisted-proof-14467
kernelpanic888:codex/simp-hoisted-proof-14467
14m 40s
CI CI #60681: Merge group checks requested
45m 1s
45m 1s
fix: ensure lean_initialize is called when Lean is only privately imported CI #60680: Pull request #14505 synchronize by Kha
19m 46s lean-initialize-module-test
lean-initialize-module-test
19m 46s