From f4d699f67d8856d57ae8ed859edb610460f17591 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Fri, 21 Aug 2026 12:38:40 +0200
Subject: [PATCH] fix: gracefully handle unknown -D options in verso-literate
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

When `lake lint` runs, it passes linter overrides to downstream executables
by prefixing the options with `weak.` (e.g., `-Dweak.linter.style.openClassical=true`).

Previously, `parseDOption` strictly relied on `getOptionDecl name` to find the
expected type for an option. If the option was unknown (e.g. because of the `weak.`
prefix or because it hasn't been registered yet), `getOptionDecl` threw an internal
exception, causing `verso-literate` to crash.

This patch mirrors the behavior of `setConfigOption` in core Lean (`src/Lean/Shell.lean`).
By using `(← getOptionDecls).find? name`, we can check if the option exists. If it does,
we parse it according to its type. If it doesn't, we gracefully fall back to storing it
as a string in the `Options` map and defer validation to the elaborator, preventing the
crash.
---
 src/verso-literate/VersoLiterateMain.lean | 50 ++++++++++++-----------
 1 file changed, 26 insertions(+), 24 deletions(-)

diff --git a/src/verso-literate/VersoLiterateMain.lean b/src/verso-literate/VersoLiterateMain.lean
index 17a51764..421f59b2 100644
--- a/src/verso-literate/VersoLiterateMain.lean
+++ b/src/verso-literate/VersoLiterateMain.lean
@@ -709,31 +709,33 @@ private def parseDOption (arg : String) (opts : Options) : IO Options := do
   | [name, value] =>
     let name := String.toName name.copy
     let value := value.copy
-    let decl ← getOptionDecl name
-    match decl.defValue with
-    | .ofBool _ =>
-      match value with
-      | "true" => return opts.setBool name true
-      | "false" => return opts.setBool name false
-      | _ => throw <| .userError s!"Invalid boolean value for option {name}: {value}"
-    | .ofNat _ =>
-      if let some n := value.toNat? then
-        return opts.insert name (DataValue.ofNat n)
-      else
-        throw <| .userError s!"Invalid natural number value for option {name}: {value}"
-    | .ofInt _ =>
-      if let some n := value.toInt? then
-        return opts.insert name (DataValue.ofInt n)
-      else
-        throw <| .userError s!"Invalid integer value for option {name}: {value}"
-    | .ofString _ =>
-      -- No quote removal needed: the shell removes quotes and interprets escapes before we see the
-      -- value
+    if let some decl := (← getOptionDecls).find? name then
+      match decl.defValue with
+      | .ofBool _ =>
+        match value with
+        | "true" => return opts.setBool name true
+        | "false" => return opts.setBool name false
+        | _ => throw <| .userError s!"Invalid boolean value for option {name}: {value}"
+      | .ofNat _ =>
+        if let some n := value.toNat? then
+          return opts.insert name (DataValue.ofNat n)
+        else
+          throw <| .userError s!"Invalid natural number value for option {name}: {value}"
+      | .ofInt _ =>
+        if let some n := value.toInt? then
+          return opts.insert name (DataValue.ofInt n)
+        else
+          throw <| .userError s!"Invalid integer value for option {name}: {value}"
+      | .ofString _ =>
+        -- No quote removal needed: the shell removes quotes and interprets escapes before we see the
+        -- value
+        return opts.insert name (DataValue.ofString value)
+      | .ofName _ =>
+        return opts.insert name (DataValue.ofName (String.toName value))
+      | .ofSyntax _ =>
+        throw <| .userError s!"Cannot set syntax-valued option {name} via -D flag"
+    else
       return opts.insert name (DataValue.ofString value)
-    | .ofName _ =>
-      return opts.insert name (DataValue.ofName (String.toName value))
-    | .ofSyntax _ =>
-      throw <| .userError s!"Cannot set syntax-valued option {name} via -D flag"
   | _ => throw <| .userError s!"Invalid -D option: {arg}"
 
 def Config.fromArgs (args : List String) : IO Config := go {mod := ""} args