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

@@ -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)

src/Lean/Language/Basic.lean

@@ -262,31 +262,60 @@ 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. -/
 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)

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<environment, object_ref> run_new_frontend(
@@ -338,7 +341,8 @@ pair_ref<environment, object_ref> run_new_frontend(
     name const & main_module_name,
     uint32_t trust_level,
     optional<std::string> const & ilean_file_name,
-    uint8_t json_output
+    uint8_t json_output,
+    array_ref<name> const & error_kinds
 ) {
     object * oilean_file_name = mk_option_none();
     if (ilean_file_name) {
@@ -352,6 +356,7 @@ pair_ref<environment, object_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<std::string> llvm_output;
     optional<std::string> root_dir;
     buffer<string_ref> forwarded_args;
+    buffer<name> 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<environment, object_ref> r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn, json_output);
+        pair_ref<environment, object_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());