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

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'.