Override Lean options

Stream: new members

[Simon Sorg]

Hey there!
I've just created a new Lean project, the first time I'm working with the toml syntax.
In the lakefile.toml, I specified lean lib, requires, and leanOptions, and would now like to add a lean exe. However, I'd like the library to be compiled with different options (such as mathlib linters) from the Lean exe.
Ideally though, I'd like to still keep the overall stronger linting requirements globally as a leanOptions section and just have a way to override it for the Lean exe specifically, just so it's cleaner.
Is this possible?

I have

name = "LeanProject"
defaultTargets = ["LeanProject"]

[leanOptions]
linter.mathlibStandardSet = true
autoImplicit = false
relaxedAutoImplicit = false
warn.sorry = false

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.25.0-rc1"

[[lean_lib]]
name = "LeanProject"
globs = ["LeanProject"]

[[lean_exe]]
name = "safe_verify"
root = "SafeVerify"
support_interpreter = true

I tried adding leanOptions = { } on the lean_exe section, but to no avail.