Skip to content

Actions: leanprover/lean4

Actions

Label PR based on Comment

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
labels-from-comments.yml
8,598 workflow runs
8,598 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

feat: asynchronous kernel checking Label PR based on Comment #9291: Issue comment #6368 (comment) created by leanprover-bot
January 18, 2025 14:20 2s
January 18, 2025 14:20 2s
feat: asynchronous kernel checking Label PR based on Comment #9290: Issue comment #6368 (comment) created by Kha
January 18, 2025 13:59 2s
January 18, 2025 13:59 2s
feat: regression tests for grind adapted from lean-egg Label PR based on Comment #9289: Issue comment #6688 (comment) created by leanprover-community-bot
January 18, 2025 12:08 2s
January 18, 2025 12:08 2s
chore: fix typo in docstring of mkMVar Label PR based on Comment #9288: Issue comment #6687 (comment) created by leanprover-community-bot
January 18, 2025 09:57 2s
January 18, 2025 09:57 2s
fix: grind parameter issues and configuration Label PR based on Comment #9287: Issue comment #6686 (comment) created by leanprover-community-bot
January 18, 2025 03:19 2s
January 18, 2025 03:19 2s
fix: make #check_failure's output be info Label PR based on Comment #9286: Issue comment #6685 (comment) created by leanprover-community-bot
January 18, 2025 03:13 1s
January 18, 2025 03:13 1s
feat: extensionality theorems in grind Label PR based on Comment #9285: Issue comment #6682 (comment) created by leanprover-community-bot
January 17, 2025 23:43 1s
January 17, 2025 23:43 1s
refactor: move ext environment extension to Lean.Meta.Tactic Label PR based on Comment #9284: Issue comment #6681 (comment) created by leodemoura
January 17, 2025 20:15 2s
January 17, 2025 20:15 2s
refactor: move ext environment extension to Lean.Meta.Tactic Label PR based on Comment #9283: Issue comment #6681 (comment) created by leodemoura
January 17, 2025 20:00 3s
January 17, 2025 20:00 3s
fix: don't generate code for decls with an implemented_by attribute Label PR based on Comment #9282: Issue comment #6680 (comment) created by leanprover-community-bot
January 17, 2025 19:47 3s
January 17, 2025 19:47 3s
fix: allow ⱼ in identifiers Label PR based on Comment #9281: Issue comment #6679 (comment) created by leanprover-community-bot
January 17, 2025 19:22 1s
January 17, 2025 19:22 1s
refactor: move ext environment extension to Lean.Meta.Tactic Label PR based on Comment #9280: Issue comment #6681 (comment) created by leanprover-community-bot
January 17, 2025 19:22 2s
January 17, 2025 19:22 2s
feat: add proper erasure of type dependencies in LCNF Label PR based on Comment #9279: Issue comment #6678 (comment) created by leanprover-community-bot
January 17, 2025 19:07 2s
January 17, 2025 19:07 2s
fix: don't generate code for decls with an implemented_by attribute Label PR based on Comment #9278: Issue comment #6680 (comment) created by zwarich
January 17, 2025 18:32 2s
January 17, 2025 18:32 2s
fix: allow ⱼ in identifiers Label PR based on Comment #9277: Issue comment #6679 (comment) created by nomeata
January 17, 2025 18:18 2s
January 17, 2025 18:18 2s
doc: clarify that lean_initialize_runtime_module is implied by lean_initialize Label PR based on Comment #9276: Issue comment #6677 (comment) created by leanprover-community-bot
January 17, 2025 17:05 3s
January 17, 2025 17:05 3s
RFC: lake add command Label PR based on Comment #9275: Issue comment #6676 (comment) created by Julian
January 17, 2025 11:49 3s
January 17, 2025 11:49 3s
perf: use C23's free_sized when available Label PR based on Comment #9274: Issue comment #6598 (comment) created by eric-wieser
January 17, 2025 11:29 3s
January 17, 2025 11:29 3s
feat: Nat.decidableBallLT handles large numbers Label PR based on Comment #9273: Issue comment #6651 (comment) created by llllvvuu
January 17, 2025 10:16 3s
January 17, 2025 10:16 3s
feat: Nat.decidableBallLT handles large numbers Label PR based on Comment #9272: Issue comment #6651 (comment) created by llllvvuu
January 17, 2025 10:08 2s
January 17, 2025 10:08 2s
feat: Nat.decidableBallLT handles large numbers Label PR based on Comment #9271: Issue comment #6651 (comment) created by nomeata
January 17, 2025 10:07 2s
January 17, 2025 10:07 2s
feat: Nat.decidableBallLT handles large numbers Label PR based on Comment #9270: Issue comment #6651 (comment) created by kim-em
January 17, 2025 09:47 3s
January 17, 2025 09:47 3s
feat: do not report metaprogramming declarations via exact? and rw? Label PR based on Comment #9269: Issue comment #6672 (comment) created by nomeata
January 17, 2025 07:39 2s
January 17, 2025 07:39 2s
feat: do not report metaprogramming declarations via exact? and rw? Label PR based on Comment #9268: Issue comment #6672 (comment) created by kim-em
January 17, 2025 07:33 2s
January 17, 2025 07:33 2s
feat: do not report metaprogramming declarations via exact? and rw? Label PR based on Comment #9267: Issue comment #6672 (comment) created by nomeata
January 17, 2025 07:32 1s
January 17, 2025 07:32 1s