`set_option maxErrors` does not work

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

set_option maxErrors inside the file has no effect when calling lean on the file, it seems to be silently ignored.

Context

This came up in the context of comparing lean lia tactic to similar proof procedures in other systems.

Steps to Reproduce

cat > maxErrors.lean << 'EOF'
set_option maxErrors 999888 -- no warning or error on this line

#check I #check I #check I #check I #check I  #check I #check I #check I #check I #check I
#check I #check I #check I #check I #check I  #check I #check I #check I #check I #check I
#check I #check I #check I #check I #check I  #check I #check I #check I #check I #check I
#check I #check I #check I #check I #check I  #check I #check I #check I #check I #check I
#check I #check I #check I #check I #check I  #check I #check I #check I #check I #check I

#check I #check I #check I #check I #check I  #check I #check I #check I #check I #check I
#check I #check I #check I #check I #check I  #check I #check I #check I #check I #check I
#check I #check I #check I #check I #check I  #check I #check I #check I #check I #check I
#check I #check I #check I #check I #check I  #check I #check I #check I #check I #check I
#check I #check I #check I #check I #check I  #check I #check I #check I #check I #check I

#check I -- :15:7: error: maximum number of errors (100; from option `maxErrors`) reached, exiting
EOF
lean maxErrors.lean # fails
lean -DmaxErrors=999999 maxErrors.lean # works

Expected behavior: the entire file is processed in both calls to lean

Actual behavior: the first lean execution stops after 100 errors

Versions

• Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)
• Lean (version 4.31.0-nightly-2026-04-29, x86_64-unknown-linux-gnu, commit 0a6c31520b2ebaa6e71227454b46ebfb4986ae7b, Release)
• OS is essentially Debian testing, perhaps lagging by a couple of months.

Start by running the minimal maxErrors.lean reproduction with both lean maxErrors.lean and lean -DmaxErrors=999999 maxErrors.lean. Trace how the set_option maxErrors 999888 command-line and in-file options are applied, then verify that the entire file is processed when the option is set in the file.