From 280fcc9883c2d3781174523ecf00d10cae4b27d6 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Fri, 13 Dec 2024 20:31:14 -0500 Subject: [PATCH] feat: `lean --error=kind` (#6362) This PR adds the `--error=kind` option (shorthand: `-Ekind`) to the `lean` CLI. When set, messages of `kind` (e.g., `linter.unusedVariables`) will be reported as errors. This setting does nothing in interactive contexts (e.g., the server). Closes #5194. The spelling `--error` was chosen instead of the common `-Werror` both for practical and behavioral reasons. Behaviorally, this option effects not just warnings, but informational messages as well. Practically, `-Werror` conflicts with the existing `-W` option for the worker and `lean` also does not currently use long single-hyphen option names. --- src/Lean/Elab/Frontend.lean | 5 ++-- src/Lean/Language/Basic.lean | 49 ++++++++++++++++++++++++++++-------- src/util/shell.cpp | 16 +++++++++--- 3 files changed, 55 insertions(+), 15 deletions(-) diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index 29f30ea51a..9f3b72982a 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/src/Lean/Elab/Frontend.lean @@ -142,6 +142,7 @@ def runFrontend (trustLevel : UInt32 := 0) (ileanFileName? : Option String := none) (jsonOutput : Bool := false) + (errorOnKinds : Array Name := #[]) : IO (Environment × Bool) := do let startTime := (← IO.monoNanosNow).toFloat / 1000000000 let inputCtx := Parser.mkInputContext input fileName @@ -150,7 +151,8 @@ def runFrontend let processor := Language.Lean.process let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel }) none ctx let snaps := Language.toSnapshotTree snap - snaps.runAndReport opts jsonOutput + let severityOverrides := errorOnKinds.foldl (·.insert · .error) {} + let hasErrors ← snaps.runAndReport opts jsonOutput severityOverrides if let some ileanFileName := ileanFileName? then let trees := snaps.getAll.flatMap (match ·.infoTree? with | some t => #[t] | _ => #[]) @@ -168,7 +170,6 @@ def runFrontend let profile ← Firefox.Profile.export mainModuleName.toString startTime traceStates opts IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile - let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors) -- no point in freeing the snapshot graph and all referenced data this close to process exit Runtime.forget snaps pure (cmdState.env, !hasErrors) diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index baa99e92d0..58894542d9 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -262,6 +262,16 @@ instance : Inhabited DynamicSnapshot where f element children.forM (·.get.forM f) +/-- + Runs a tree of snapshots to conclusion, + folding the function `f` over each snapshot in tree preorder. -/ +@[specialize] partial def SnapshotTree.foldM [Monad m] (s : SnapshotTree) + (f : α → Snapshot → m α) (init : α) : m α := do + match s with + | mk element children => + let a ← f init element + children.foldlM (fun a snap => snap.get.foldM f a) a + /-- Option for printing end position of each message in addition to start position. Used for testing message ranges in the test suite. -/ @@ -269,24 +279,43 @@ register_builtin_option printMessageEndPos : Bool := { defValue := false, descr := "print end position of each message in addition to start position" } -/-- Reports messages on stdout. If `json` is true, prints messages as JSON (one per line). -/ -def reportMessages (msgLog : MessageLog) (opts : Options) (json := false) : IO Unit := do - if json then - msgLog.forM (·.toJson <&> (·.compress) >>= IO.println) - else - msgLog.forM (·.toString (includeEndPos := printMessageEndPos.get opts) >>= IO.print) +/-- +Reports messages on stdout and returns whether an error was reported. +If `json` is true, prints messages as JSON (one per line). +If a message's kind is in `severityOverrides`, it will be reported with +the specified severity. +-/ +def reportMessages (msgLog : MessageLog) (opts : Options) + (json := false) (severityOverrides : NameMap MessageSeverity := {}) : IO Bool := do + let includeEndPos := printMessageEndPos.get opts + msgLog.unreported.foldlM (init := false) fun hasErrors msg => do + let msg : Message := + if let some severity := severityOverrides.find? msg.kind then + {msg with severity} + else + msg + if json then + let j ← msg.toJson + IO.println j.compress + else + let s ← msg.toString includeEndPos + IO.print s + return hasErrors || msg.severity matches .error /-- Runs a tree of snapshots to conclusion and incrementally report messages on stdout. Messages are - reported in tree preorder. + reported in tree preorder. Returns whether any errors were reported. This function is used by the cmdline driver; see `Lean.Server.FileWorker.reportSnapshots` for how the language server reports snapshots asynchronously. -/ -def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (json := false) : IO Unit := do - s.forM (reportMessages ·.diagnostics.msgLog opts json) +def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) + (json := false) (severityOverrides : NameMap MessageSeverity := {}) : IO Bool := do + s.foldM (init := false) fun e snap => do + let e' ← reportMessages snap.diagnostics.msgLog opts json severityOverrides + return strictOr e e' /-- Waits on and returns all snapshots in the tree. -/ def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot := - s.forM (m := StateM _) (fun s => modify (·.push s)) |>.run #[] |>.2 + Id.run <| s.foldM (·.push ·) #[] /-- Returns a task that waits on all snapshots in the tree. -/ def SnapshotTree.waitAll : SnapshotTree → BaseIO (Task Unit) diff --git a/src/util/shell.cpp b/src/util/shell.cpp index 02027d0265..a39ca0b658 100644 --- a/src/util/shell.cpp +++ b/src/util/shell.cpp @@ -223,6 +223,7 @@ static void display_help(std::ostream & out) { std::cout << " --plugin=file load and initialize Lean shared library for registering linters etc.\n"; std::cout << " --load-dynlib=file load shared library to make its symbols available to the interpreter\n"; std::cout << " --json report Lean output (e.g., messages) as JSON (one per line)\n"; + std::cout << " -E --error=kind report Lean messages of kind as errors\n"; std::cout << " --deps just print dependencies of a Lean input\n"; std::cout << " --print-prefix print the installation prefix for Lean and exit\n"; std::cout << " --print-libdir print the installation directory for Lean's built-in libraries and exit\n"; @@ -268,6 +269,7 @@ static struct option g_long_options[] = { #endif {"plugin", required_argument, 0, 'p'}, {"load-dynlib", required_argument, 0, 'l'}, + {"error", required_argument, 0, 'E'}, {"json", no_argument, &json_output, 1}, {"print-prefix", no_argument, &print_prefix, 1}, {"print-libdir", no_argument, &print_libdir, 1}, @@ -278,7 +280,7 @@ static struct option g_long_options[] = { }; static char const * g_opt_str = - "PdD:o:i:b:c:C:qgvVht:012j:012rR:M:012T:012ap:e" + "PdD:o:i:b:c:C:qgvVht:012j:012rR:M:012T:012ap:eE:" #if defined(LEAN_MULTI_THREAD) "s:012" #endif @@ -330,6 +332,7 @@ extern "C" object * lean_run_frontend( uint32_t trust_level, object * ilean_filename, uint8_t json_output, + object * error_kinds, object * w ); pair_ref run_new_frontend( @@ -338,7 +341,8 @@ pair_ref run_new_frontend( name const & main_module_name, uint32_t trust_level, optional const & ilean_file_name, - uint8_t json_output + uint8_t json_output, + array_ref const & error_kinds ) { object * oilean_file_name = mk_option_none(); if (ilean_file_name) { @@ -352,6 +356,7 @@ pair_ref run_new_frontend( trust_level, oilean_file_name, json_output, + error_kinds.to_obj_arg(), io_mk_world() )); } @@ -475,6 +480,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { optional llvm_output; optional root_dir; buffer forwarded_args; + buffer error_kinds; while (true) { int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL); @@ -597,6 +603,10 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { lean::load_dynlib(optarg); forwarded_args.push_back(string_ref("--load-dynlib=" + std::string(optarg))); break; + case 'E': + check_optarg("E"); + error_kinds.push_back(string_to_name(std::string(optarg))); + break; default: std::cerr << "Unknown command line option\n"; display_help(std::cerr); @@ -705,7 +715,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { if (!main_module_name) main_module_name = name("_stdin"); - pair_ref r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn, json_output); + pair_ref r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn, json_output, error_kinds); env = r.fst(); bool ok = unbox(r.snd().raw());