set maxsynthpendingdepth in toml

Stream: general

[Kevin Buzzard]

After a bump to mathlib changing a definition, I suddenly find that FLT needs a bunch of set_option maxSynthPendingDepth 2. Like mathlib, I'd like to set this globally in the project. But mathlib has a lakefile.lean and I have a lakefile.toml so I can't just naively copy. Mathlib seems to have

abbrev mathlibLeanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`autoImplicit, false⟩,
    ⟨`maxSynthPendingDepth, .ofNat 3⟩
  ] ++ -- options that are used in `lake build`
    mathlibOnlyLinters.map fun s ↦ { s with name := `weak ++ s.name }

and then

@[default_target]
lean_lib Mathlib where
  -- Enforce Mathlib's default linters and style options.
  leanOptions := mathlibLeanOptions

How do I translate this into toml-language? Right now I have

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
autoImplicit = false # no "assume a typo is a new variable"
relaxedAutoImplicit = false # no "assume a typo is a new variable"
linter.style.longLine = true # no lines longer than 100 chars
linter.oldObtain = true # no "stream of consciousness `obtain`"
linter.style.cases = true # no `cases'` tactic
linter.style.refine = true # no `refine'` tactic
linter.style.multiGoal = true # no multiple active goals
weak.linter.flexible = true # no rigid tactic (e.g. `exact`) after a flexible tactic (e.g. `simp`)

and I would just have a guess but I'm unsure about the ofNat thing and don't really like fiddling with these files without expert guidance.

[Henrik Böving]

I think it should be possible to just set maxSynthPendingDepth = 3. At least I've done this with numeric options in the past and it worked.