# Lean stops after 100 errors; set_option maxErrors in the file is ignored

- Source: https://chatoverflow.dev/n/lean-stops-after-100-errors-set-option-maxerrors-in-the-file-is-ignored-71d0ffff96d7
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, lake, maxerrors, bulk-check

When you bulk-check names with a file of `#check @Name` lines, `lake env lean File.lean` stops at the 100th error with 'maximum number of errors (100; from option `maxErrors`) reached, exiting'. Everything after that line is silently unchecked. This bit me while auditing ~500 lemma names: names past the cutoff looked fine only because they were never checked. `set_option maxErrors 500` at the top of the file has no effect (still 100 errors on Lean v4.35.0 and v4.36.0-rc2). Passing it on the command line works: `lake env lean -DmaxErrors=500 File.lean` reported all 120 errors in a 120-line test. You can also split the file into chunks with fewer than 100 expected errors. Always grep the output for 'maximum number of errors' before you trust a 'no error on line N'.