From 87c123bb1bc54a850e583ea5e2eb79b8a5051070 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Wed, 22 Apr 2026 19:17:41 +0100 Subject: [PATCH] feat: lake: add support for running environment linters (#13431) This PR adds builtin environment linting support to Lake, accessible via `lake lint` flags. It also introduces two builtin linters upstreamed from Mathlib (`defLemma` and `checkUnivs`) and a `builtinLint` package configuration option. Builtin linting is triggered via flags on `lake lint`: - `--builtin-lint`: run default builtin linters (in addition to the lint driver if configured) - `--builtin-only`: run only builtin linters, skip the lint driver - `--clippy`: run only non-default (clippy) linters - `--lint-all`: run all builtin linters (default + clippy) - `--lint-only `: run a specific builtin linter by name - Using `--clippy`, `--lint-all`, or `--lint-only` implicitly enables builtin lint mode The `builtinLint` package option is a tristate (`Option Bool`): - `true`: always run builtin lints via `lake lint`; when a lint driver is also configured, builtin lints run first, then the driver, and the command fails if either reports errors. - `false`: never run builtin lints automatically; `lake check-lint` fails unless a lint driver is configured. - `none` (default): currently equivalent to `false`; in a future release, `none` will fall back to builtin lints when no lint driver is configured. The linter framework introduces a `LintScope` enum (`.default`, `.clippy`, `.all`) replacing the previous boolean `clippy` parameter in `getChecks` and `formatLinterResults`. A `@[builtin_nolint]` attribute (available without imports) allows suppressing specific linters per declaration. --------- Co-authored-by: Mac Malone Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com> --- src/Init.lean | 1 + src/Init/Linter.lean | 15 ++ src/Lean/Elab/DeclModifiers.lean | 1 + src/Lean/Linter/EnvLinter.lean | 1 + src/Lean/Linter/EnvLinter/Basic.lean | 26 +-- src/Lean/Linter/EnvLinter/Builtin.lean | 102 ++++++++++++ src/Lean/Linter/EnvLinter/Frontend.lean | 36 +++-- src/Lean/Linter/EnvLinter/Nolint.lean | 35 +++++ src/lake/Lake/CLI/BuiltinLint.lean | 69 ++++++++ src/lake/Lake/CLI/Help.lean | 30 +++- src/lake/Lake/CLI/Main.lean | 56 ++++++- src/lake/Lake/Config/PackageConfig.lean | 13 ++ src/lake/schemas/lakefile-toml-schema.json | 4 + tests/CMakeLists.txt | 1 + tests/elab/env_linter.lean | 73 +++++++-- tests/lake/tests/builtin-lint/Clean.lean | 4 + .../tests/builtin-lint/ClippyViolations.lean | 4 + tests/lake/tests/builtin-lint/Linters.lean | 12 ++ tests/lake/tests/builtin-lint/Main.lean | 24 +++ tests/lake/tests/builtin-lint/clean.sh | 3 + .../lake/tests/builtin-lint/input/Clean.lean | 4 + .../builtin-lint/input/ClippyViolations.lean | 4 + .../tests/builtin-lint/input/Linters.lean | 12 ++ tests/lake/tests/builtin-lint/input/Main.lean | 24 +++ .../tests/builtin-lint/input/lakefile.toml | 14 ++ tests/lake/tests/builtin-lint/lakefile.toml | 14 ++ tests/lake/tests/builtin-lint/lean-toolchain | 1 + tests/lake/tests/builtin-lint/test.sh | 148 ++++++++++++++++++ .../lake/tests/builtin-lint/with-driver.lean | 15 ++ 29 files changed, 684 insertions(+), 62 deletions(-) create mode 100644 src/Init/Linter.lean create mode 100644 src/Lean/Linter/EnvLinter/Builtin.lean create mode 100644 src/Lean/Linter/EnvLinter/Nolint.lean create mode 100644 src/lake/Lake/CLI/BuiltinLint.lean create mode 100644 tests/lake/tests/builtin-lint/Clean.lean create mode 100644 tests/lake/tests/builtin-lint/ClippyViolations.lean create mode 100644 tests/lake/tests/builtin-lint/Linters.lean create mode 100644 tests/lake/tests/builtin-lint/Main.lean create mode 100755 tests/lake/tests/builtin-lint/clean.sh create mode 100644 tests/lake/tests/builtin-lint/input/Clean.lean create mode 100644 tests/lake/tests/builtin-lint/input/ClippyViolations.lean create mode 100644 tests/lake/tests/builtin-lint/input/Linters.lean create mode 100644 tests/lake/tests/builtin-lint/input/Main.lean create mode 100644 tests/lake/tests/builtin-lint/input/lakefile.toml create mode 100644 tests/lake/tests/builtin-lint/lakefile.toml create mode 100644 tests/lake/tests/builtin-lint/lean-toolchain create mode 100755 tests/lake/tests/builtin-lint/test.sh create mode 100644 tests/lake/tests/builtin-lint/with-driver.lean diff --git a/src/Init.lean b/src/Init.lean index 83f23e37a5..e4ffdd3b3a 100644 --- a/src/Init.lean +++ b/src/Init.lean @@ -48,3 +48,4 @@ public import Init.BinderNameHint public import Init.Task public import Init.MethodSpecsSimp public import Init.LawfulBEqTactics +public import Init.Linter diff --git a/src/Init/Linter.lean b/src/Init/Linter.lean new file mode 100644 index 0000000000..4ca1d4e643 --- /dev/null +++ b/src/Init/Linter.lean @@ -0,0 +1,15 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Różowski +-/ +module + +prelude +public import Init.Notation + +public section + +/-- `@[builtin_nolint linterName*]` omits the tagged declaration from being checked by +the named builtin linters in `lake builtin-lint`. -/ +syntax (name := builtin_nolint) "builtin_nolint" (ppSpace ident)+ : attr diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index 23d2737074..ad43c494ee 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -8,6 +8,7 @@ module prelude public import Lean.DocString.Add public import Lean.Linter.Basic +import Lean.Linter.EnvLinter.Nolint meta import Lean.Parser.Command public section diff --git a/src/Lean/Linter/EnvLinter.lean b/src/Lean/Linter/EnvLinter.lean index 959cbc78b7..11bd92abd5 100644 --- a/src/Lean/Linter/EnvLinter.lean +++ b/src/Lean/Linter/EnvLinter.lean @@ -8,3 +8,4 @@ module prelude public import Lean.Linter.EnvLinter.Basic public import Lean.Linter.EnvLinter.Frontend +public import Lean.Linter.EnvLinter.Builtin diff --git a/src/Lean/Linter/EnvLinter/Basic.lean b/src/Lean/Linter/EnvLinter/Basic.lean index 520fb8a0f8..5575f091ed 100644 --- a/src/Lean/Linter/EnvLinter/Basic.lean +++ b/src/Lean/Linter/EnvLinter/Basic.lean @@ -13,6 +13,7 @@ prelude public import Lean.Structure public import Lean.Elab.InfoTree.Main import Lean.ExtraModUses +public import Lean.Linter.EnvLinter.Nolint public section @@ -135,29 +136,4 @@ builtin_initialize registerBuiltinAttribute { modifyEnv fun env => envLinterExt.addEntry env (decl, dflt) } -/-- `@[builtin_nolint linterName]` omits the tagged declaration from being checked by -the linter with name `linterName`. -/ -syntax (name := builtin_nolint) "builtin_nolint" (ppSpace ident)+ : attr - -/-- Defines the user attribute `builtin_nolint` for skipping environment linters. -/ -builtin_initialize builtinNolintAttr : ParametricAttribute (Array Name) ← - registerParametricAttribute { - name := `builtin_nolint - descr := "Do not report this declaration in any of the tests of `lake builtin-lint`" - getParam := fun _ => fun - | `(attr| builtin_nolint $[$ids]*) => ids.mapM fun id => withRef id <| do - let shortName := id.getId.eraseMacroScopes - let some (declName, _) := (envLinterExt.getState (← getEnv)).find? shortName - | throwError "linter '{shortName}' not found" - Elab.addConstInfo id declName - recordExtraModUseFromDecl (isMeta := false) declName - pure shortName - | _ => Elab.throwUnsupportedSyntax - } - -/-- Returns true if `decl` should be checked -using `linter`, i.e., if there is no `builtin_nolint` attribute. -/ -def shouldBeLinted [Monad m] [MonadEnv m] (linter : Name) (decl : Name) : m Bool := - return !((builtinNolintAttr.getParam? (← getEnv) decl).getD #[]).contains linter - end Lean.Linter.EnvLinter diff --git a/src/Lean/Linter/EnvLinter/Builtin.lean b/src/Lean/Linter/EnvLinter/Builtin.lean new file mode 100644 index 0000000000..565599d449 --- /dev/null +++ b/src/Lean/Linter/EnvLinter/Builtin.lean @@ -0,0 +1,102 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Różowski + +Copyright (c) 2020 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner +-/ +module + +prelude +public meta import Lean.Linter.EnvLinter.Basic +public meta import Lean.MonadEnv +public meta import Lean.ReducibilityAttrs +public meta import Lean.ProjFns +public meta import Lean.Meta.InferType +public meta import Lean.Util.CollectLevelParams +public meta import Lean.Util.ForEachExpr +public meta import Lean.Meta.Instances + +open Lean Meta + +public meta section + +namespace Lean.Linter.EnvLinter + +/-- A linter for checking whether the correct declaration constructor (`def` or `theorem`) +has been used. A `def` whose type is a `Prop` should be a `theorem`, and vice versa. -/ +@[builtin_env_linter] def defLemma : EnvLinter where + noErrorsFound := "All declarations correctly marked as def/lemma." + errorsFound := "INCORRECT DEF/LEMMA:" + test declName := do + if ← isAutoDecl declName then return none + let info ← getConstInfo declName + if info.isDefinition then + if ← isProp info.type then return some "is a def, should be a lemma/theorem" + return none + +/-- +`univParamsGrouped e nm₀` computes for each `Level` occurring in `e` the set of level parameters +that appear in it, returning the collection of such parameter sets. +In pseudo-mathematical form, this returns `{{p : parameter | p ∈ u} | (u : level) ∈ e}`. +Ignores `nm₀.proof_*` sub-constants. +-/ +private def univParamsGrouped (e : Expr) (nm₀ : Name) : Std.HashSet (Array Name) := + runST fun σ => do + let res ← ST.mkRef (σ := σ) {} + e.forEach fun + | .sort u => + res.modify (·.insert (CollectLevelParams.visitLevel u {}).params) + | .const n us => do + if let .str n s .. := n then + if n == nm₀ && s.startsWith "proof_" then + return + res.modify <| us.foldl (·.insert <| CollectLevelParams.visitLevel · {} |>.params) + | _ => pure () + res.get + +/-- +The good parameters are the parameters that occur somewhere in the set as a singleton or +(recursively) with only other good parameters. +All other parameters in the set are bad. +-/ +private partial def badParams (l : Array (Array Name)) : Array Name := + let goodLevels := l.filterMap fun + | #[u] => some u + | _ => none + if goodLevels.isEmpty then + l.flatten.toList.eraseDups.toArray + else + badParams <| l.map (·.filter (!goodLevels.contains ·)) + +/-- A linter for checking that there are no bad `max u v` universe levels. +Checks whether all universe levels `u` in the type of `d` are "good". +This means that `u` either occurs in a `Level` of `d` by itself, or (recursively) +with only other good levels. +When this fails, usually this means that there is a level `max u v`, where neither `u` nor `v` +occur by themselves in a level. It is ok if *one* of `u` or `v` never occurs alone. For example, +`(α : Type u) (β : Type (max u v))` is an occasionally useful method of saying that `β` lives in +a higher universe level than `α`. -/ +@[builtin_env_linter] def checkUnivs : EnvLinter where + noErrorsFound := + "All declarations have good universe levels." + errorsFound := "THE STATEMENTS OF THE FOLLOWING DECLARATIONS HAVE BAD UNIVERSE LEVELS. \ + This usually means that there is a `max u v` in the type where neither `u` nor `v` \ + occur by themselves. Solution: Find the type (or type bundled with data) that has this \ + universe argument and provide the universe level explicitly. If this happens in an implicit \ + argument of the declaration, a better solution is to move this argument to a `variables` \ + command (then it's not necessary to provide the universe level).\n\n\ + It is possible that this linter gives a false positive on definitions where the value of the \ + definition has the universes occur separately, and the definition will usually be used with \ + explicit universe arguments. In this case, feel free to add `@[builtin_nolint checkUnivs]`." + test declName := do + if ← isAutoDecl declName then return none + let bad := badParams (univParamsGrouped (← getConstInfo declName).type declName).toArray + if bad.isEmpty then return none + return m!"universes {bad} only occur together." + +end Lean.Linter.EnvLinter + +end diff --git a/src/Lean/Linter/EnvLinter/Frontend.lean b/src/Lean/Linter/EnvLinter/Frontend.lean index 61586960ba..bf514dcf09 100644 --- a/src/Lean/Linter/EnvLinter/Frontend.lean +++ b/src/Lean/Linter/EnvLinter/Frontend.lean @@ -32,18 +32,33 @@ inductive LintVerbosity | high deriving Inhabited, DecidableEq, Repr -/-- `getChecks clippy runOnly` produces a list of linters. -`runOnly` is an optional list of names that should resolve to declarations with type -`NamedEnvLinter`. If populated, only these linters are run (regardless of the default -configuration). Otherwise, it uses all enabled linters in the environment tagged with -`@[builtin_env_linter]`. If `clippy` is false, it only uses linters with `isDefault = true`. -/ -def getChecks (clippy : Bool) (runOnly : Option (List Name)) : +/-- Which set of linters to run. -/ +inductive LintScope + /-- Run only default linters. -/ + | default + /-- Run only non-default (clippy) linters. -/ + | clippy + /-- Run all linters (default + clippy). -/ + | all + deriving Inhabited, DecidableEq, Repr + +/-- `getChecks` produces a list of linters to run. + +If `runOnly` is populated, only those named linters are run (regardless of `scope`). +Otherwise, linter selection depends on `scope`: +- `default`: only linters with `isDefault = true` +- `clippy`: only linters with `isDefault = false` +- `all`: all linters -/ +def getChecks (scope : LintScope := .default) (runOnly : Option (List Name) := none) : CoreM (Array NamedEnvLinter) := do let mut result := #[] for (name, declName, isDefault) in envLinterExt.getState (← getEnv) do let shouldRun := match runOnly with | some only => only.contains name - | none => clippy || isDefault + | none => match scope with + | .default => isDefault + | .clippy => !isDefault + | .all => true if shouldRun then let linter ← getEnvLinter name declName result := result.binInsert (·.name.lt ·.name) linter @@ -133,7 +148,7 @@ def formatLinterResults (results : Array (NamedEnvLinter × Std.HashMap Name MessageData)) (decls : Array Name) (groupByFilename : Bool) - (whereDesc : String) (runClippyLinters : Bool) + (whereDesc : String) (scope : LintScope := .default) (verbose : LintVerbosity) (numLinters : Nat) (useErrorFormat : Bool := false) : CoreM MessageData := do let formattedResults ← results.filterMapM fun (linter, results) => do @@ -156,7 +171,10 @@ def formatLinterResults } in {decls.size - numAutoDecls} declarations (plus { numAutoDecls} automatically generated ones) {whereDesc } with {numLinters} linters\n\n{s}" - unless runClippyLinters do s := m!"{s}-- (non-clippy linters skipped)\n" + match scope with + | .default => s := m!"{s}-- (non-default linters skipped)\n" + | .clippy => s := m!"{s}-- (default linters skipped)\n" + | .all => pure () pure s /-- Get the list of declarations in the current module. -/ diff --git a/src/Lean/Linter/EnvLinter/Nolint.lean b/src/Lean/Linter/EnvLinter/Nolint.lean new file mode 100644 index 0000000000..4dd0aaab2c --- /dev/null +++ b/src/Lean/Linter/EnvLinter/Nolint.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Różowski + +Copyright (c) 2020 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner +-/ +module + +prelude +public import Lean.Attributes +import Init.Linter + +public section + +namespace Lean.Linter.EnvLinter + +/-- Defines the user attribute `builtin_nolint` for skipping environment linters. -/ +builtin_initialize builtinNolintAttr : ParametricAttribute (Array Name) ← + registerParametricAttribute { + name := `builtin_nolint + descr := "Do not report this declaration in any of the tests of `lake builtin-lint`" + getParam := fun _ => fun + | `(attr| builtin_nolint $[$ids]*) => pure <| ids.map (·.getId.eraseMacroScopes) + | _ => Elab.throwUnsupportedSyntax + } + +/-- Returns true if `decl` should be checked +using `linter`, i.e., if there is no `builtin_nolint` attribute. -/ +def shouldBeLinted [Monad m] [MonadEnv m] (linter : Name) (decl : Name) : m Bool := + return !((builtinNolintAttr.getParam? (← getEnv) decl).getD #[]).contains linter + +end Lean.Linter.EnvLinter diff --git a/src/lake/Lake/CLI/BuiltinLint.lean b/src/lake/Lake/CLI/BuiltinLint.lean new file mode 100644 index 0000000000..ac4fa1aab3 --- /dev/null +++ b/src/lake/Lake/CLI/BuiltinLint.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Różowski +-/ +module + +prelude +public import Lean.Linter.EnvLinter +import Lean.CoreM +import Lake.Config.Workspace + +open Lean Lean.Core Meta + +namespace Lake.BuiltinLint + +/-- Arguments for builtin linting via `lake lint --builtin-lint`. -/ +public structure Args where + /-- Which set of linters to run (set by `--clippy` / `--lint-all`; default if neither). -/ + scope : Linter.EnvLinter.LintScope := .default + /-- Run only the specified linters. -/ + only : Array Name := #[] + /-- Skip the up-to-date build check. -/ + force : Bool := false + /-- The list of root modules to lint. -/ + mods : Array Name := #[] + +/-- +Run the builtin environment linters on the given modules. + +Assumes Lean's search path has already been properly configured. +-/ +public def run (args : Args) : IO UInt32 := do + let mods := args.mods + if mods.isEmpty then + IO.eprintln "lake lint: no modules specified for builtin linting" + return 1 + + let runOnly := if args.only.isEmpty then none else some args.only.toList + let scope := args.scope + let envLinterModule : Import := { module := `Lean.Linter.EnvLinter } + + let mut anyFailed := false + for mod in mods do + unsafe Lean.enableInitializersExecution + let env ← importModules #[{ module := mod }, envLinterModule] {} (trustLevel := 1024) (loadExts := true) + let (result, _) ← CoreM.toIO (ctx := { fileName := "", fileMap := default }) (s := { env }) do + let decls ← Linter.EnvLinter.getDeclsInPackage mod.getRoot + let linters ← Linter.EnvLinter.getChecks (scope := scope) (runOnly := runOnly) + if linters.isEmpty then + IO.println s!"-- No linters registered for {mod}." + return false + let results ← Linter.EnvLinter.lintCore decls linters + let failed := results.any (!·.2.isEmpty) + if failed then + let fmtResults ← + Linter.EnvLinter.formatLinterResults results decls + (groupByFilename := true) (useErrorFormat := true) + s!"in {mod}" (scope := if args.only.isEmpty then scope else .all) .medium linters.size + IO.print (← fmtResults.toString) + else + IO.println s!"-- Linting passed for {mod}." + return failed + if result then + anyFailed := true + + return if anyFailed then 1 else 0 + +end Lake.BuiltinLint diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index 0835e062b4..bfacf95ce0 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -26,7 +26,7 @@ COMMANDS: check-build check if any default build targets are configured test test the package using the configured test driver check-test check if there is a properly configured test driver - lint lint the package using the configured lint driver + lint lint the package check-lint check if there is a properly configured lint driver clean remove build outputs shake minimize imports in source files @@ -242,17 +242,33 @@ package or its dependencies. It merely verifies that one is specified. " def helpLint := -"Lint the workspace's root package using its configured lint driver +"Lint the workspace's root package USAGE: - lake lint [-- ...] + lake lint [OPTIONS] [...] [-- ...] + +By default, runs the package's configured lint driver. If `builtinLint` is +set to `true` in the package configuration, builtin lints also run. + +Positional `MODULE` arguments narrow only the builtin lints; if omitted, +the workspace's default target roots are used. The lint driver is invoked +with `lintDriverArgs` from the package config plus any arguments after +`--`; the `MODULE` list is not passed to it. + +OPTIONS: + --builtin-lint run builtin environment linters + --builtin-only run only builtin linters, skip the lint driver + --clippy run only non-default (clippy) builtin linters + --lint-all run all builtin linters (default + clippy) + --lint-only run only the specified builtin linter (repeatable) + --force skip the up-to-date build check A lint driver can be configured by either setting the `lintDriver` package -configuration option by tagging a script or executable `@[lint_driver]`. -A definition in dependency can be used as a test driver by using the -`/` syntax for the 'testDriver' configuration option. +configuration option or by tagging a script or executable `@[lint_driver]`. +A definition in a dependency can be used as a lint driver by using the +`/` syntax for the 'lintDriver' configuration option. -A script lint driver will be run with the package configuration's +A script lint driver will be run with the package configuration's `lintDriverArgs` plus the CLI `args`. An executable lint driver will be built and then run like a script. " diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index ad03940333..5a126d15a5 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -27,6 +27,7 @@ import Lake.CLI.Build import Lake.CLI.Actions import Lake.CLI.Translate import Lake.CLI.Serve +public import Lake.CLI.BuiltinLint import Init.Data.String.Modify -- # CLI @@ -72,6 +73,11 @@ public structure LakeOptions where rev? : Option GitRev := none maxRevs : Nat := 100 shake : Shake.Args := {} + builtinLint : BuiltinLint.Args := {} + /-- Whether `lake lint` should also run builtin lints (via `--builtin-lint`). -/ + runBuiltinLint : Bool := false + /-- Whether `lake lint` should skip the lint driver (via `--builtin-only`). -/ + builtinOnly : Bool := false def LakeOptions.outLv (opts : LakeOptions) : LogLevel := opts.outLv?.getD opts.verbosity.minLogLv @@ -302,12 +308,24 @@ def lakeLongOption : (opt : String) → CliM PUnit | "--" => do let subArgs ← takeArgs modifyThe LakeOptions ({· with subArgs}) +-- Builtin lint options (using any of these implicitly enables --builtin-lint) +| "--builtin-lint" => modifyThe LakeOptions ({· with runBuiltinLint := true}) +| "--builtin-only" => modifyThe LakeOptions ({· with runBuiltinLint := true, builtinOnly := true}) +| "--clippy" => modifyThe LakeOptions ({· with + runBuiltinLint := true, builtinLint.scope := .clippy, builtinLint.only := #[]}) +| "--lint-all" => modifyThe LakeOptions ({· with + runBuiltinLint := true, builtinLint.scope := .all, builtinLint.only := #[]}) +| "--lint-only" => do + let name ← takeOptArg "--lint-only" "linter name" + modifyThe LakeOptions fun opts => + {opts with runBuiltinLint := true, builtinLint.only := opts.builtinLint.only.push name.toName} +-- Shared options +| "--force" => modifyThe LakeOptions ({· with shake.force := true, builtinLint.force := true}) -- Shake options | "--keep-implied" => modifyThe LakeOptions ({· with shake.keepImplied := true}) | "--keep-prefix" => modifyThe LakeOptions ({· with shake.keepPrefix := true}) | "--keep-public" => modifyThe LakeOptions ({· with shake.keepPublic := true}) | "--add-public" => modifyThe LakeOptions ({· with shake.addPublic := true}) -| "--force" => modifyThe LakeOptions ({· with shake.force := true}) | "--gh-style" => modifyThe LakeOptions ({· with shake.githubStyle := true}) | "--explain" => modifyThe LakeOptions ({· with shake.explain := true}) | "--trace" => modifyThe LakeOptions ({· with shake.trace := true}) @@ -945,18 +963,46 @@ protected def checkTest : CliM PUnit := do let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions)) noArgsRem do exit <| if pkg.testDriver.isEmpty then 1 else 0 +private def runBuiltinLint + (ws : Workspace) (args : BuiltinLint.Args) (mods : Array Lean.Name) : CliM UInt32 := do + let mods := if mods.isEmpty then ws.defaultTargetRoots else mods + if mods.isEmpty then + error "no modules specified and there are no applicable default targets" + let args := {args with mods} + unless args.force do + let specs ← parseTargetSpecs ws (mods.map (s!"+{·}") |>.toList) + let upToDate ← ws.checkNoBuild <| buildSpecs specs + unless upToDate do + error "there are out of date oleans; run `lake build` or fetch them from a cache first" + Lean.searchPathRef.set ws.augmentedLeanPath + BuiltinLint.run args + protected def lint : CliM PUnit := do processOptions lakeOption let opts ← getThe LakeOptions let ws ← loadWorkspace (← mkLoadConfig opts) - noArgsRem do - let x := ws.root.lint opts.subArgs (mkBuildConfig opts) - exit <| ← x.run (mkLakeContext ws) + let hasDriver := !ws.root.lintDriver.isEmpty && !opts.builtinOnly + let pkgBuiltinLint := ws.root.config.builtinLint? + let doBuiltinLint := opts.runBuiltinLint || pkgBuiltinLint == some true + let mut exitCode : UInt32 := 0 + if doBuiltinLint then + let mods := (← takeArgs).toArray.map (·.toName) + exitCode ← runBuiltinLint ws opts.builtinLint mods + if hasDriver then + let driverExitCode ← noArgsRem do + ws.root.lint opts.subArgs (mkBuildConfig opts) |>.run (mkLakeContext ws) + unless driverExitCode == 0 do + exitCode := driverExitCode + unless doBuiltinLint || hasDriver do + error s!"no lint driver configured and builtin linting is disabled" + exit exitCode protected def checkLint : CliM PUnit := do processOptions lakeOption let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions)) - noArgsRem do exit <| if pkg.lintDriver.isEmpty then 1 else 0 + noArgsRem do + let hasLint := !pkg.lintDriver.isEmpty || pkg.config.builtinLint? == some true + exit <| if hasLint then 0 else 1 protected def clean : CliM PUnit := do processOptions lakeOption diff --git a/src/lake/Lake/Config/PackageConfig.lean b/src/lake/Lake/Config/PackageConfig.lean index 76ef81be9a..22b08dea9b 100644 --- a/src/lake/Lake/Config/PackageConfig.lean +++ b/src/lake/Lake/Config/PackageConfig.lean @@ -321,6 +321,19 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig -/ allowImportAll : Bool := false + /-- + Whether to run Lake's built-in linter on the package. + + * `true` — Always run built-in lints. When a lint driver is also configured, + built-in lints run before the driver. + * `false` — Never run built-in lints by default. `lake check-lint` will exit + with a nonzero code if no lint driver is configured either. + * `none` (default) — Currently equivalent to `false`. In a future release, `none` + will run built-in lints when no lint driver is configured (i.e., act like `true` + as a fallback). + -/ + builtinLint?, builtinLint : Option Bool := none + /-- Whether this package is expected to function only on a single toolchain (the package's toolchain). diff --git a/src/lake/schemas/lakefile-toml-schema.json b/src/lake/schemas/lakefile-toml-schema.json index 94bae79efb..8a0dd832f0 100644 --- a/src/lake/schemas/lakefile-toml-schema.json +++ b/src/lake/schemas/lakefile-toml-schema.json @@ -568,6 +568,10 @@ "default": [], "description": "Arguments to pass to the package's linter.\nThese arguments will come before those passed on the command line via `lake lint -- ...`." }, + "builtinLint": { + "type": "boolean", + "description": "Whether to run Lake's built-in linter on the package.\n\n* `true` — Always run built-in lints. When a lint driver is also configured, built-in lints run before the driver.\n* `false` — Never run built-in lints by default. `lake check-lint` will exit with a nonzero code if no lint driver is configured either.\n* unset (the default) — Currently equivalent to `false`. In a future release, an unset value will run built-in lints when no lint driver is configured (i.e., act like `true` as a fallback)." + }, "releaseRepo": { "type": "string", "description": "The URL of the GitHub repository to upload and download releases of this package.\nIf not set, for downloads, Lake uses the URL the package was download from (if it is a dependency) and for uploads, uses `gh`'s default." diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index ae58a4842f..9b183682e4 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -261,6 +261,7 @@ else() GLOB_RECURSE LEANLAKETESTS "${LEAN_SOURCE_DIR}/../tests/lake/examples/test.sh" "${LEAN_SOURCE_DIR}/../tests/lake/tests/shake/test.sh" + "${LEAN_SOURCE_DIR}/../tests/lake/tests/builtin-lint/test.sh" ) endif() foreach(T ${LEANLAKETESTS}) diff --git a/tests/elab/env_linter.lean b/tests/elab/env_linter.lean index 13d2e20bce..36589659b1 100644 --- a/tests/elab/env_linter.lean +++ b/tests/elab/env_linter.lean @@ -127,26 +127,35 @@ error: invalid attribute `builtin_env_linter`, linter `dummyBadName` has already -- Default mode: only isDefault=true linters def testGetChecksDefault : CoreM (Array Name) := do - let checks ← getChecks (clippy := false) (runOnly := none) + let checks ← getChecks (scope := .default) (runOnly := none) return checks.map (·.name) --- dummyBadName is default, dummyClippyLinter is not -/-- info: #[`dummyBadName] -/ +-- dummyBadName and checkUnivs are default, dummyClippyLinter is not +/-- info: #[`checkUnivs, `defLemma, `dummyBadName] -/ #guard_msgs in #eval testGetChecksDefault --- Clippy mode: all linters +-- Clippy mode: only non-default linters def testGetChecksClippy : CoreM (Array Name) := do - let checks ← getChecks (clippy := true) (runOnly := none) + let checks ← getChecks (scope := .clippy) (runOnly := none) return checks.map (·.name) -/-- info: #[`dummyBadName, `dummyClippyLinter] -/ +/-- info: #[`dummyClippyLinter] -/ #guard_msgs in #eval testGetChecksClippy +-- All mode: all linters +def testGetChecksAll : CoreM (Array Name) := do + let checks ← getChecks (scope := .all) (runOnly := none) + return checks.map (·.name) + +/-- info: #[`checkUnivs, `defLemma, `dummyBadName, `dummyClippyLinter] -/ +#guard_msgs in +#eval testGetChecksAll + -- runOnly: only specified linters def testGetChecksRunOnly : CoreM (Array Name) := do - let checks ← getChecks (clippy := false) (runOnly := some [`dummyClippyLinter]) + let checks ← getChecks (runOnly := some [`dummyClippyLinter]) return checks.map (·.name) /-- info: #[`dummyClippyLinter] -/ @@ -168,17 +177,17 @@ def testDeclsInCurrModule : CoreM Bool := do -- lintCore should find badDef but not goodDef or badButNolinted def testLintCore : CoreM (Array (Name × Nat)) := do - let linters ← getChecks (clippy := false) (runOnly := none) + let linters ← getChecks (scope := .default) (runOnly := none) let results ← lintCore #[`badDef, `goodDef, `badButNolinted] linters return results.map fun (linter, msgs) => (linter.name, msgs.size) -/-- info: #[(`dummyBadName, 1)] -/ +/-- info: #[(`checkUnivs, 0), (`defLemma, 0), (`dummyBadName, 1)] -/ #guard_msgs in #eval testLintCore -- Verify which declaration was flagged def testLintCoreDetail : CoreM (Array Name) := do - let linters ← getChecks (clippy := false) (runOnly := none) + let linters ← getChecks (scope := .default) (runOnly := none) let results ← lintCore #[`badDef, `goodDef, `badButNolinted] linters let mut flagged := #[] for (_, msgs) in results do @@ -193,15 +202,15 @@ def testLintCoreDetail : CoreM (Array Name) := do /-! ## Test: formatLinterResults -/ def testFormatResults : CoreM Format := do - let linters ← getChecks (clippy := false) (runOnly := none) + let linters ← getChecks (scope := .default) (runOnly := none) let results ← lintCore #[`badDef, `goodDef] linters let msg ← formatLinterResults results #[`badDef, `goodDef] - (groupByFilename := false) (whereDesc := "in test") (runClippyLinters := true) + (groupByFilename := false) (whereDesc := "in test") (scope := .all) (verbose := .medium) (numLinters := linters.size) return (← msg.format) /-- -info: -- Found 1 error in 2 declarations (plus 0 automatically generated ones) in test with 1 linters +info: -- Found 1 error in 2 declarations (plus 0 automatically generated ones) in test with 3 linters /- The `dummyBadName` linter reports: found bad names -/ @@ -212,15 +221,47 @@ found bad names -/ -- No errors case def testFormatResultsClean : CoreM Format := do - let linters ← getChecks (clippy := false) (runOnly := none) + let linters ← getChecks (scope := .default) (runOnly := none) let results ← lintCore #[`goodDef] linters let msg ← formatLinterResults results #[`goodDef] - (groupByFilename := false) (whereDesc := "in test") (runClippyLinters := true) + (groupByFilename := false) (whereDesc := "in test") (scope := .all) (verbose := .medium) (numLinters := linters.size) return (← msg.format) /-- -info: -- Found 0 errors in 1 declarations (plus 0 automatically generated ones) in test with 1 linters +info: -- Found 0 errors in 1 declarations (plus 0 automatically generated ones) in test with 3 linters -/ #guard_msgs in #eval testFormatResultsClean + +/-! ## Test: checkUnivs -/ + +-- Good: each universe parameter occurs alone somewhere +universe u v in +def goodUnivs (α : Type u) (β : Type v) : Type (max u v) := α × β + +-- Good: one universe dominates the other (max u v where u occurs alone) +universe u v in +def goodUnivsDominated (α : Type u) (β : Type (max u v)) : Type (max u v) := α × β + +-- Bad: neither u nor v occur alone +universe u v in +def badUnivs (α : Type (max u v)) : Type (max u v) := α + +def testCheckUnivs (declName : Name) : MetaM Bool := do + let some (linterDeclName, _) := (envLinterExt.getState (← getEnv)).find? `checkUnivs + | throwError "not found" + let linter ← getEnvLinter `checkUnivs linterDeclName + return (← linter.test declName).isSome + +/-- info: false -/ +#guard_msgs in +#eval testCheckUnivs `goodUnivs + +/-- info: false -/ +#guard_msgs in +#eval testCheckUnivs `goodUnivsDominated + +/-- info: true -/ +#guard_msgs in +#eval testCheckUnivs `badUnivs diff --git a/tests/lake/tests/builtin-lint/Clean.lean b/tests/lake/tests/builtin-lint/Clean.lean new file mode 100644 index 0000000000..f7949c4026 --- /dev/null +++ b/tests/lake/tests/builtin-lint/Clean.lean @@ -0,0 +1,4 @@ +-- No linter violations here. +theorem correctTheorem : 1 = 1 := rfl + +def correctDef : Nat := 42 diff --git a/tests/lake/tests/builtin-lint/ClippyViolations.lean b/tests/lake/tests/builtin-lint/ClippyViolations.lean new file mode 100644 index 0000000000..b4e9c015e7 --- /dev/null +++ b/tests/lake/tests/builtin-lint/ClippyViolations.lean @@ -0,0 +1,4 @@ +import Linters + +-- This name ends with 'Clippy' — the dummyClippy linter should flag it. +def badNameClippy : Nat := 1 diff --git a/tests/lake/tests/builtin-lint/Linters.lean b/tests/lake/tests/builtin-lint/Linters.lean new file mode 100644 index 0000000000..56f4eda6eb --- /dev/null +++ b/tests/lake/tests/builtin-lint/Linters.lean @@ -0,0 +1,12 @@ +import Lean.Linter.EnvLinter + +open Lean Meta + +-- A dummy clippy linter that flags any declaration whose name ends with "Clippy". +@[builtin_env_linter clippy] public meta def dummyClippy : Lean.Linter.EnvLinter.EnvLinter where + noErrorsFound := "No declarations ending with 'Clippy' found." + errorsFound := "CLIPPY VIOLATIONS:" + test declName := do + if declName.toString.endsWith "Clippy" then + return some "declaration name ends with 'Clippy'" + return none diff --git a/tests/lake/tests/builtin-lint/Main.lean b/tests/lake/tests/builtin-lint/Main.lean new file mode 100644 index 0000000000..d4a85b8fae --- /dev/null +++ b/tests/lake/tests/builtin-lint/Main.lean @@ -0,0 +1,24 @@ +-- This uses `def` for a Prop — the `defLemma` linter should flag this. +def shouldBeTheorem : 1 = 1 := rfl + +-- This is annotated to be skipped by `defLemma` — no import needed. +@[builtin_nolint defLemma] +def skippedViolation : 2 = 2 := rfl + +-- A `@[reducible, instance] def` of Prop type is still elaborated as a `def`, +-- so `defLemma` should flag it. +@[reducible, instance] +def reducibleInstShouldBeTheorem : Nonempty Bool := ⟨true⟩ + +-- A plain `instance` of Prop type is elaborated as a `theorem`, so it should +-- not be flagged. +instance plainInstIsOk : Nonempty String := ⟨""⟩ + +-- Bad universe levels — the `checkUnivs` linter should flag this. +universe u v in +def badUnivDecl (α : Type (max u v)) : Type (max u v) := α + +-- Annotated to be skipped by `checkUnivs`. +universe u v in +@[builtin_nolint checkUnivs] +def badUnivSkipped (α : Type (max u v)) : Type (max u v) := α diff --git a/tests/lake/tests/builtin-lint/clean.sh b/tests/lake/tests/builtin-lint/clean.sh new file mode 100755 index 0000000000..ed07cb2816 --- /dev/null +++ b/tests/lake/tests/builtin-lint/clean.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +rm -rf .lake +rm -f lakefile.toml lake-manifest.json Main.lean Clean.lean Linters.lean ClippyViolations.lean diff --git a/tests/lake/tests/builtin-lint/input/Clean.lean b/tests/lake/tests/builtin-lint/input/Clean.lean new file mode 100644 index 0000000000..f7949c4026 --- /dev/null +++ b/tests/lake/tests/builtin-lint/input/Clean.lean @@ -0,0 +1,4 @@ +-- No linter violations here. +theorem correctTheorem : 1 = 1 := rfl + +def correctDef : Nat := 42 diff --git a/tests/lake/tests/builtin-lint/input/ClippyViolations.lean b/tests/lake/tests/builtin-lint/input/ClippyViolations.lean new file mode 100644 index 0000000000..b4e9c015e7 --- /dev/null +++ b/tests/lake/tests/builtin-lint/input/ClippyViolations.lean @@ -0,0 +1,4 @@ +import Linters + +-- This name ends with 'Clippy' — the dummyClippy linter should flag it. +def badNameClippy : Nat := 1 diff --git a/tests/lake/tests/builtin-lint/input/Linters.lean b/tests/lake/tests/builtin-lint/input/Linters.lean new file mode 100644 index 0000000000..56f4eda6eb --- /dev/null +++ b/tests/lake/tests/builtin-lint/input/Linters.lean @@ -0,0 +1,12 @@ +import Lean.Linter.EnvLinter + +open Lean Meta + +-- A dummy clippy linter that flags any declaration whose name ends with "Clippy". +@[builtin_env_linter clippy] public meta def dummyClippy : Lean.Linter.EnvLinter.EnvLinter where + noErrorsFound := "No declarations ending with 'Clippy' found." + errorsFound := "CLIPPY VIOLATIONS:" + test declName := do + if declName.toString.endsWith "Clippy" then + return some "declaration name ends with 'Clippy'" + return none diff --git a/tests/lake/tests/builtin-lint/input/Main.lean b/tests/lake/tests/builtin-lint/input/Main.lean new file mode 100644 index 0000000000..d4a85b8fae --- /dev/null +++ b/tests/lake/tests/builtin-lint/input/Main.lean @@ -0,0 +1,24 @@ +-- This uses `def` for a Prop — the `defLemma` linter should flag this. +def shouldBeTheorem : 1 = 1 := rfl + +-- This is annotated to be skipped by `defLemma` — no import needed. +@[builtin_nolint defLemma] +def skippedViolation : 2 = 2 := rfl + +-- A `@[reducible, instance] def` of Prop type is still elaborated as a `def`, +-- so `defLemma` should flag it. +@[reducible, instance] +def reducibleInstShouldBeTheorem : Nonempty Bool := ⟨true⟩ + +-- A plain `instance` of Prop type is elaborated as a `theorem`, so it should +-- not be flagged. +instance plainInstIsOk : Nonempty String := ⟨""⟩ + +-- Bad universe levels — the `checkUnivs` linter should flag this. +universe u v in +def badUnivDecl (α : Type (max u v)) : Type (max u v) := α + +-- Annotated to be skipped by `checkUnivs`. +universe u v in +@[builtin_nolint checkUnivs] +def badUnivSkipped (α : Type (max u v)) : Type (max u v) := α diff --git a/tests/lake/tests/builtin-lint/input/lakefile.toml b/tests/lake/tests/builtin-lint/input/lakefile.toml new file mode 100644 index 0000000000..40455136b4 --- /dev/null +++ b/tests/lake/tests/builtin-lint/input/lakefile.toml @@ -0,0 +1,14 @@ +name = "lint" +defaultTargets = ["Main", "Clean", "Linters", "ClippyViolations"] + +[[lean_lib]] +name = "Main" + +[[lean_lib]] +name = "Clean" + +[[lean_lib]] +name = "Linters" + +[[lean_lib]] +name = "ClippyViolations" diff --git a/tests/lake/tests/builtin-lint/lakefile.toml b/tests/lake/tests/builtin-lint/lakefile.toml new file mode 100644 index 0000000000..40455136b4 --- /dev/null +++ b/tests/lake/tests/builtin-lint/lakefile.toml @@ -0,0 +1,14 @@ +name = "lint" +defaultTargets = ["Main", "Clean", "Linters", "ClippyViolations"] + +[[lean_lib]] +name = "Main" + +[[lean_lib]] +name = "Clean" + +[[lean_lib]] +name = "Linters" + +[[lean_lib]] +name = "ClippyViolations" diff --git a/tests/lake/tests/builtin-lint/lean-toolchain b/tests/lake/tests/builtin-lint/lean-toolchain new file mode 100644 index 0000000000..38df318ac4 --- /dev/null +++ b/tests/lake/tests/builtin-lint/lean-toolchain @@ -0,0 +1 @@ +../../../../../build/release/stage1 \ No newline at end of file diff --git a/tests/lake/tests/builtin-lint/test.sh b/tests/lake/tests/builtin-lint/test.sh new file mode 100755 index 0000000000..811b8b6cac --- /dev/null +++ b/tests/lake/tests/builtin-lint/test.sh @@ -0,0 +1,148 @@ +#!/usr/bin/env bash +source ../common.sh + +./clean.sh +cp -r input/* . + +# --builtin-lint should fail with a clear message when oleans are not built +lake_out lint --builtin-lint || true +match_pat 'out of date oleans' produced.out + +# up-to-date check is per-module: building only Clean should let us lint Clean +test_run build Clean +test_run lint --builtin-only Clean + +# but linting Main (not yet built) should still fail the up-to-date check +lake_out lint --builtin-only Main || true +match_pat 'out of date oleans' produced.out + +test_run build + +# --builtin-lint should detect the defLemma violation in Main (the default target) +lake_out lint --builtin-lint || true +match_pat 'shouldBeTheorem' produced.out +match_pat 'is a def, should be a lemma/theorem' produced.out +# `@[reducible, instance]` on a `def` of Prop type keeps it a `def`, so flag it. +match_pat 'reducibleInstShouldBeTheorem' produced.out +# Plain `instance` of Prop type is elaborated as a theorem; it should not be flagged. +no_match_pat 'plainInstIsOk' produced.out + +# --builtin-lint should also detect the checkUnivs violation +match_pat 'badUnivDecl' produced.out +match_pat 'only occur together' produced.out +# builtin_nolint checkUnivs should suppress the warning +no_match_pat 'badUnivSkipped' produced.out + +# --lint-only defLemma should run only the defLemma linter +lake_out lint --lint-only defLemma || true +match_pat 'shouldBeTheorem' produced.out +no_match_pat 'badUnivDecl' produced.out + +# Clean module has no violations; exit code should be 0 +test_run lint --builtin-only Clean + +# Without --clippy, the clippy linter should not run +lake_out lint --builtin-only ClippyViolations || true +no_match_pat 'badNameClippy' produced.out + +# --clippy should run only non-default (clippy) linters +lake_out lint --clippy ClippyViolations || true +match_pat 'badNameClippy' produced.out +match_pat "declaration name ends with 'Clippy'" produced.out +# --clippy should not run default linters +no_match_pat 'shouldBeTheorem' produced.out + +# --lint-all should run both default and clippy linters +lake_out lint --lint-all ClippyViolations || true +match_pat 'badNameClippy' produced.out + +# Multiple --lint-only flags accumulate: both named linters should run +lake_out lint --lint-only defLemma --lint-only checkUnivs || true +match_pat 'shouldBeTheorem' produced.out +match_pat 'badUnivDecl' produced.out +no_match_pat 'badNameClippy' produced.out + +# Last-wins: --clippy overrides a prior --lint-all and clears --lint-only +lake_out lint --lint-all --lint-only defLemma --clippy || true +match_pat 'badNameClippy' produced.out +no_match_pat 'shouldBeTheorem' produced.out +no_match_pat 'badUnivDecl' produced.out + +# Last-wins: --lint-all overrides a prior --clippy (both default and clippy run) +lake_out lint --clippy --lint-all || true +match_pat 'badNameClippy' produced.out +match_pat 'shouldBeTheorem' produced.out + +# Last-wins: --clippy clears a previously accumulated --lint-only +lake_out lint --lint-only defLemma --clippy || true +match_pat 'badNameClippy' produced.out +no_match_pat 'shouldBeTheorem' produced.out + +# --lint-only after --clippy: the named linter runs (selection ignores scope) +lake_out lint --clippy --lint-only defLemma || true +match_pat 'shouldBeTheorem' produced.out +no_match_pat 'badNameClippy' produced.out + +# --builtin-only should skip the lint driver +lake_out lint -f with-driver.lean --builtin-only Main || true +match_pat 'shouldBeTheorem' produced.out +no_match_pat 'lint-driver:' produced.out + +# --- builtinLint package configuration tests --- + +# Default (builtinLint unset / none): check-lint fails (same as false for now) +test_fails check-lint + +# Default: lake lint errors when no lintDriver and builtinLint is unset +lake_out lint || true +match_pat 'no lint driver configured' produced.out + +# Default: lake lint --builtin-lint overrides and runs builtin lints +lake_out lint --builtin-lint || true +match_pat 'shouldBeTheorem' produced.out + +# --clippy implicitly enables builtin lint +lake_out lint --clippy ClippyViolations || true +match_pat 'badNameClippy' produced.out + +# --lint-only implicitly enables builtin lint +lake_out lint --lint-only defLemma || true +match_pat 'shouldBeTheorem' produced.out + +# builtinLint = false: check-lint fails (no lint driver and builtin linting disabled) +sed_i 's/^name = .*/&\nbuiltinLint = false/' lakefile.toml +test_fails check-lint + +# builtinLint = false: lake lint errors +lake_out lint || true +match_pat 'no lint driver configured' produced.out + +# builtinLint = false with --builtin-lint flag: overrides and runs builtin lints +lake_out lint --builtin-lint || true +match_pat 'shouldBeTheorem' produced.out + +# builtinLint = true: check-lint succeeds even without a lint driver +sed_i 's/builtinLint = false/builtinLint = true/' lakefile.toml +test_run check-lint + +# builtinLint = true: lake lint runs builtin lints +lake_out lint || true +match_pat 'shouldBeTheorem' produced.out + +# Restore original lakefile +cp input/lakefile.toml lakefile.toml + +# --- builtinLint = true with a lint driver --- + +# builtinLint = true + lint driver + clean module: both builtin lints and driver run +lake_out lint -f with-driver.lean Clean || true +match_pat 'Linting passed for Clean' produced.out +match_pat 'lint-driver:' produced.out + +# builtinLint = true + lint driver + violations: both run, exit code is nonzero +lake_out lint -f with-driver.lean Main || true +match_pat 'shouldBeTheorem' produced.out +match_pat 'lint-driver:' produced.out + +# builtinLint = true + lint driver: check-lint succeeds +test_run -f with-driver.lean check-lint diff --git a/tests/lake/tests/builtin-lint/with-driver.lean b/tests/lake/tests/builtin-lint/with-driver.lean new file mode 100644 index 0000000000..737061cd97 --- /dev/null +++ b/tests/lake/tests/builtin-lint/with-driver.lean @@ -0,0 +1,15 @@ +import Lake +open System Lake DSL + +package lint where + builtinLint := true + +@[lint_driver] +script lintDriver args do + IO.println s!"lint-driver: {args}" + return 0 + +lean_lib Main +lean_lib Clean +lean_lib Linters +lean_lib ClippyViolations