fix: gracefully handle unknown -D options in verso-literate

src/errata-tests/fixtures/driver-bare/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.35.0-rc2
+leanprover/lean4:v4.35.0-rc3

src/errata-tests/fixtures/driver-configured/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.35.0-rc2
+leanprover/lean4:v4.35.0-rc3

src/errata-tests/fixtures/driver-shadowed/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.35.0-rc2
+leanprover/lean4:v4.35.0-rc3

src/tests/VersoTests/LiterateHtml.lean

@@ -1279,8 +1279,25 @@ private def testMultiRootNavTree (data : TestData) : Test := withTestDir data fu
   assertContains "<details" navbarSection
     "multi-root nav: navbar should use <details> for top-level entries"
 
+/--
+Library options with the {lit}`weak.` prefix take effect during literate extraction.
+-/
+-- `LibB` sets `weak.linter.unusedVariables = false` and a `weak.` option that isn't
+-- registered. Each library has a definition with an unused variable. The warning appears in the
+-- JSON for `LibA.Core` and does not in the JSON for {lit}`LibB.Utils`.
+
+private def testWeakLeanOptions (data : TestData) : Test := do
+  let warning := "linter.unusedVariables"
+  let libA ← IO.FS.readFile (jsonPath data.jsonDir "LibA.Core")
+  assertContains warning libA
+    "LibA.Core JSON has no unused variable warning, so the test module does not trigger the linter"
+  let libB ← IO.FS.readFile (jsonPath data.jsonDir "LibB.Utils")
+  assertNotContains warning libB
+    "LibB.Utils JSON has an unused variable warning, so `weak.linter.unusedVariables` had no effect"
+
 private def multiRootHtmlTests (data : TestData) : List (String × Test) := [
-  ("multi-root nav tree", testMultiRootNavTree data)
+  ("multi-root nav tree", testMultiRootNavTree data),
+  ("weak lean options", testWeakLeanOptions data)
 ]
 
 /-- The literate HTML generator produces the expected output for the multi-root test project. -/

src/verso-literate/VersoLiterateMain.lean

@@ -643,6 +643,8 @@ unsafe def go (suppressedNamespaces : Array Name) (extraImports : Array Name) (m
     let imports := headerToImports headerStx
     enableInitializersExecution
     let env ← Compat.importModules (extraImports.map ({module := ·}) ++ imports) {}
+    -- Rewrite `weak.` options based on the definitions discovered during imports
+    let leanOptions ← Lean.Language.Lean.reparseOptions leanOptions
     let pctx : Frontend.Context := {inputCtx := ictx}
 
     let opts := leanOptions.mergeBy (fun _ _ v => v) (maxHeartbeats.set {} 10000000)
@@ -699,8 +701,9 @@ structure Config where
   leanOptions : Options := {}
 
 /--
-Parses a `-Dname=value` flag into a Lean option, registering it in `opts`.
-Uses the registered option declaration to determine the expected type.
+Parses a `-Dname=value` flag into a Lean option, registering it in `opts`.  A registered option's
+value is parsed according to its declaration. Other options are stored as strings, to be parsed
+after their declarations have been imported.
 -/
 private def parseDOption (arg : String) (opts : Options) : IO Options := do
   let arg := arg.drop 2  -- drop "-D"
@@ -709,31 +712,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

test-projects/literate-multi-root/LibA/Core.lean

@@ -6,3 +6,6 @@ Some core definitions for library A.
 
 /-- Doubles a number. -/
 def doubleA (n : Nat) : Nat := n * 2
+
+/-- Ignores its argument. The `unusedVariables` linter warns about `ignoreA`. -/
+def ignoreA (n : Nat) : Nat := 0

test-projects/literate-multi-root/LibB/Utils.lean

@@ -6,3 +6,9 @@ Some utility definitions for library B.
 
 /-- Triples a number. -/
 def tripleB (n : Nat) : Nat := n * 3
+
+/--
+Ignores its argument. The library options for `LibB` disable the `unusedVariables` linter with a
+`weak.` option, so `ignoreB` should have no warning.
+-/
+def ignoreB (n : Nat) : Nat := 0

test-projects/literate-multi-root/lakefile.toml

@@ -10,3 +10,4 @@ name = "LibA"
 
 [[lean_lib]]
 name = "LibB"
+leanOptions = {weak.linter.unusedVariables = false, weak.verso.test.nonexistent = true}