Repository navigation

Make every Lean warning a compile error (warningAsError, like Tau Ceti) - #751

Merged

Vilin97 merged 3 commits into

mainfrom

vasil/warning-as-error

Nov 6, 2026

Merged

Make every Lean warning a compile error (warningAsError, like Tau Ceti)#751
Vilin97 merged 3 commits into
mainfrom
vasil/warning-as-error

Commits on Nov 5, 2026
- Make every Lean warning a compile error
  
  Vilin97
  and
  claude
  committed
  8e2afaf
- Keep the banned option token out of the lakefile comment
  
  Vilin97
  and
  claude
  committed
  a5c83b0
Commits on Nov 6, 2026
- Keep warning policy compatible with proof-length documentation
  Vilin97
  authored
  63a15b5