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: add [grind homo] attribute Backport #21043: Pull request #14446 closed by leodemoura
10s
10s
feat: add [grind homo] attribute Backport #21042: Pull request #14446 labeled by leodemoura
Skipped
Skipped
fix: pretty printing of @[simp ←] Backport #21041: Pull request #14367 closed by nomeata
8s
8s
test: for issues #14440 Backport #21040: Pull request #14445 closed by leodemoura
5s
5s
fix: avoid expensive isDefEqD in grind Backport #21039: Pull request #14444 closed by leodemoura
5s
5s
test: for issues #14440 Backport #21038: Pull request #14445 labeled by leodemoura
Skipped
Skipped
fix: avoid expensive isDefEqD in grind Backport #21037: Pull request #14444 labeled by leodemoura
1s
1s
fix: restore ambient exporting scope in mkAuxDefinition Backport #21036: Pull request #14442 closed by Kha
8s
8s
fix: restore ambient exporting scope in mkAuxDefinition Backport #21035: Pull request #14442 labeled by leanprover-bot
1s
1s
fix: restore ambient exporting scope in mkAuxDefinition Backport #21034: Pull request #14442 labeled by Kha
9s
9s
fix: don't resynthesize unwrapped nested proofs in the grind canonicalizer Backport #21033: Pull request #14439 closed by leodemoura
5s
5s
fix: don't resynthesize unwrapped nested proofs in the grind canonicalizer Backport #21032: Pull request #14439 labeled by leodemoura
1s
1s
fix: don't expose inferInstanceAs wrapping aux defs for non-exposed types Backport #21031: Pull request #14437 labeled by mathlib-lean-pr-testing Bot
11s
11s
fix: don't expose inferInstanceAs wrapping aux defs for non-exposed types Backport #21030: Pull request #14437 closed by Kha
5s
5s
fix: don't expose inferInstanceAs wrapping aux defs for non-exposed types Backport #21029: Pull request #14437 labeled by Kha
1s
1s
refactor: drive lattice saturation with Sym.simp rewriting Backport #21028: Pull request #14434 closed by sgraf812
8s
8s
fix: over-specialized backward rules in vcgen's spec rule cache Backport #21027: Pull request #14431 closed by sgraf812
6s
6s
doc: drop internal-lemma references from repeatM docstrings Backport #21026: Pull request #14436 labeled by sgraf812
11s
11s
refactor: drop the structural-combinator fast path in vcgen Backport #21025: Pull request #14433 closed by sgraf812
6s
6s
feat: look for .ilean.mmap files on watchdog load Backport #21024: Pull request #14421 labeled by robsimmons
1s
1s
refactor: drive lattice saturation with Sym.simp rewriting Backport #21023: Pull request #14434 labeled by sgraf812
7s
7s
refactor: drop the structural-combinator fast path in vcgen Backport #21022: Pull request #14433 labeled by sgraf812
1s
1s
feat: forbid non-reserved identifiers via withForbidden Backport #21021: Pull request #14432 labeled by sgraf812
8s
8s
feat: apply specs with conjunctive preconditions without frame inference Backport #21020: Pull request #14383 closed by sgraf812
6s
6s
fix: over-specialized backward rules in vcgen's spec rule cache Backport #21019: Pull request #14431 labeled by sgraf812
9s
9s