invalid -D parameter, lean v4.19.0-rc2

Stream: mathlib4

[Asei Inoue]

I updated my Lean version from v4.18.0 to v4.19.0-rc2 and now I get the following error. I have no idea how to fix it, so please help me.

invalid -D parameter, unknown configuration option 'linter.flexible'

If the option is defined in this library, use '-Dweak.linter.flexible' to set it conditionally

[Asei Inoue]

my lakefile:

import Lake
open Lake DSL

abbrev linterOptions : Array LeanOption := #[
  ⟨`linter.flexible, true⟩,
  ⟨`linter.oldObtain, true⟩,
  ⟨`linter.style.cdot, true⟩,
  ⟨`linter.style.dollarSyntax, true⟩,
  ⟨`linter.style.missingEnd, true⟩,
  ⟨`linter.style.lambdaSyntax, true⟩,
  ⟨`structureDiamondWarning, true⟩
]

package «Lean by Example» where
  keywords := #[]
  description := "foo bar"
  leanOptions := #[
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩
  ] ++ linterOptions.map (fun s ↦ {s with name := `weak ++ s.name})
  moreServerOptions := linterOptions

[Kyle Miller]

It means you don't have Mathlib.Tactic.Linter.FlexibleLinter imported.

Another way to fix it is to disable setting the option by commenting out ⟨`linter.flexible, true⟩,

[Asei Inoue]

thank you

[David Renshaw]

I suspect something deeper is broken with linters on v4.19.0-rc2.
I tried running lake exe runLinter on my project and it seemed to not run any linter at all. (Usually it gives me tons of warnings.)

[Kim Morrison]

@David Renshaw, is there a repro I can run? Likely this is the same problem as affected doc-gen4.

[David Renshaw]

lake exe runLinter Compfiles in https://github.com/dwrensha/compfiles

[David Renshaw]

@Kim Morrison ^

[David Renshaw]

My guess is that it has to do with withImportModules no longer loading env extensions.

[Kim Morrison]

I needed

lake exe cache get
lake build
lake exe runLinter Compfiles

but indeed yes, no output.

[Kim Morrison]

And setting loadExts := true in runLinter fixes it.

[Kim Morrison]

batteries#1190

[Kim Morrison]

@Sebastian Ullrich, I think at this point I agree that loadExts should not have a default value. What do you think?

[Sebastian Ullrich]

Ah, that sounds like a good compromise

[Asei Inoue]

(removed)

[Asei Inoue]

(removed)

[Anne Baanen]

This error now also appears if I try to edit files at the bottom of the Mathlib hierarchy, such as Mathlib/Tactic/Linter/Lint.lean.

[Anne Baanen]

The files compile fine, so I think the issue is with the moreServerOptions in the lakefile:

/-- These options are used
* as `leanOptions`, prefixed by `` `weak``, so that `lake build` uses them;
* as `moreServerArgs`, to set their default value in mathlib
  (as well as `Archive`, `Counterexamples` and `test`). -/
abbrev mathlibOnlyLinters : Array LeanOption := #[
  -- The `docPrime` linter is disabled: https://github.com/leanprover-community/mathlib4/issues/20560
  ⟨`linter.docPrime, false⟩,
  ⟨`linter.hashCommand, true⟩,
  ⟨`linter.oldObtain, true⟩,
  ⟨`linter.style.cases, true⟩,
  ⟨`linter.style.cdot, true⟩,
  ⟨`linter.style.docString, true⟩,
  ⟨`linter.style.dollarSyntax, true⟩,
  ⟨`linter.style.header, true⟩,
  ⟨`linter.style.lambdaSyntax, true⟩,
  ⟨`linter.style.longLine, true⟩,
  ⟨`linter.style.longFile, .ofNat 1500⟩,
  -- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
  ⟨`linter.style.missingEnd, true⟩,
  ⟨`linter.style.multiGoal, true⟩,
  ⟨`linter.style.openClassical, true⟩,
  ⟨`linter.style.refine, true⟩,
  ⟨`linter.style.setOption, true⟩
]

/-- These options are passed as `leanOptions` to building mathlib, as well as the
`Archive` and `Counterexamples`. (`tests` omits the first two options.) -/
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 }

...

@[default_target]
lean_lib Mathlib where
  leanOptions := mathlibLeanOptions
  -- Mathlib also enforces these linter options, which are not active by default.
  moreServerOptions := mathlibOnlyLinters

So probably we should set moreServerOptions to either mathlibOnlyLinters.map fun s ↦ { s with name := `weak ++ s.name } or empty (since they are all set in mathlibLeanOptions anyway).

[Sebastian Ullrich]

This may be unintentional (but ultimately consistent) breakage from #7376, which fortunately suggests a much easier fix: you can simply delete the moreServerOptions and it should work fine now

[Anne Baanen]

(I assume you mean lean4#7376?)

[Anne Baanen]

Looks like the moreServerOptions are indeed unneeded, and removing them fixes the issue. I'll open a PR removing them from Mathlib.

[Anne Baanen]

#23667