Repository navigation

refactor(Tactic/Linter/Header): make the header linter stateful - #42201

Open

marcelolynch wants to merge 17 commits into

leanprover-community:masterfrom

marcelolynch:2026/07/HeaderStateful

Open

refactor(Tactic/Linter/Header): make the header linter stateful#42201
marcelolynch wants to merge 17 commits into
leanprover-community:masterfrom
marcelolynch:2026/07/HeaderStateful

Commits on Jul 28, 2026
- refactor(Tactic/Linter/MinImports): make the minImports linter stateful
  
  marcelolynch
  and
  claude
  committed
  37280a9
- test(MinImports): pin linter behavior under parallel elaboration
  
  marcelolynch
  and
  claude
  committed
  fec2cfa
- doc(Tactic/Linter/MinImports): link the upstreaming PR for withSetOptionIn'
  
  marcelolynch
  and
  claude
  committed
  c1dbc65
- doc(Tactic/Linter/MinImports): note possible reset semantics for #import_bumps
  
  marcelolynch
  and
  claude
  committed
  e8cad37
- refactor(Tactic/Linter/Header): make the header linter stateful
  
  marcelolynch
  and
  claude
  committed
  de82606
- doc(Tactic/Linter/Header): link the upstreaming PR for withSetOptionIn'
  
  marcelolynch
  and
  claude
  committed
  3799adf
- feat(Tactic/Linter/Header): store the parsed header in the linter state
  
  marcelolynch
  and
  claude
  committed
  d9be336
- refactor(Tactic/Linter/MinImports): read the parsed header from the header linter state
  
  marcelolynch
  and
  claude
  committed
  6f2cb49
- refactor(Tactic/Linter/Style): read the parsed header in the longLine linter
  
  marcelolynch
  and
  claude
  committed
  a314edf
Commits on Aug 11, 2026
- Merge remote-tracking branch 'upstream/master' into 2026/07/MinImportsStateful
  marcelolynch
  committed
  01bbc4a
- refactor(Tactic/Linter/MinImports): use `withSetOptionIn` from core
  
  marcelolynch
  and
  claude
  committed
  a2fe021
- Merge branch '2026/07/MinImportsStateful' into 2026/07/HeaderStateful
  marcelolynch
  committed
  de901b9
- refactor(Tactic/Linter): use `withSetOptionIn` from core
  
  marcelolynch
  and
  claude
  committed
  e84aa33
- fix(Tactic/Linter/MinImports): import `Mathlib.Init` for the header state
  
  marcelolynch
  and
  claude
  committed
  aa0366f
Commits on Aug 14, 2026
- Merge remote-tracking branch 'upstream/master' into 2026/07/HeaderStateful
  marcelolynch
  committed
  6580b44
Commits on Sep 2, 2026
- Merge remote-tracking branch 'upstream/master' into 2026/07/HeaderStateful
  marcelolynch
  committed
  cde957f
- refactor(Tactic/Linter/Header): make the new header linter implementation stateful
  
  marcelolynch
  and
  claude
  committed
  48540ad

Commits

Commits on Jul 28, 2026

Commits on Aug 11, 2026

Commits on Aug 14, 2026

Commits on Sep 2, 2026