feat: accept user-defined options on the cmdline (#4741)

Initial options are now re-parsed and validated after importing. Cmdline
option assignments prefixed with `weak.` are silently discarded if the
option name without the prefix does not exist.

Fixes #3403

src/Lean/Elab/Frontend.lean

@@ -132,6 +132,47 @@ def process (input : String) (env : Environment) (opts : Options) (fileName : Op
   let s ← IO.processCommands inputCtx { : Parser.ModuleParserState } (Command.mkState env {} opts)
   pure (s.commandState.env, s.commandState.messages)
 
+/--
+Parses values of options registered during import and left by the C++ frontend as strings, fails if
+any option names remain unknown.
+-/
+def reparseOptions (opts : Options) : IO Options := do
+  let mut opts := opts
+  let decls ← getOptionDecls
+  for (name, val) in opts do
+    let .ofString val := val
+      | continue  -- Already parsed by C++
+    -- Options can be prefixed with `weak` in order to turn off the error when the option is not
+    -- defined
+    let weak := name.getRoot == `weak
+    if weak then
+      opts := opts.erase name
+    let name := name.replacePrefix `weak Name.anonymous
+    let some decl := decls.find? name
+      | unless weak do
+          throw <| .userError s!"invalid -D parameter, unknown configuration option '{name}'
+          
+If the option is defined in this library, use '-D{`weak ++ name}' to set it conditionally"
+
+    match decl.defValue with
+    | .ofBool _ =>
+      match val with
+      | "true"  => opts := opts.insert name true
+      | "false" => opts := opts.insert name false
+      | _ =>
+        throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
+          it must be true/false"
+    | .ofNat _ =>
+      let some val := val.toNat?
+        | throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
+            it must be a natural number"
+      opts := opts.insert name val
+    | .ofString _ => opts := opts.insert name val
+    | _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
+              cannot be set in the command line, use set_option command"
+
+  return opts
+
 @[export lean_run_frontend]
 def runFrontend
     (input : String)
@@ -151,6 +192,8 @@ def runFrontend
     let (header, parserState, messages) ← Parser.parseHeader inputCtx
     -- allow `env` to be leaked, which would live until the end of the process anyway
     let (env, messages) ← processHeader (leakEnv := true) header opts messages inputCtx trustLevel
+    -- now that imports have been loaded, check options again
+    let opts ← reparseOptions opts
     let env := env.setMainModule mainModuleName
     let mut commandState := Command.mkState env messages opts
     let elabStartTime := (← IO.monoNanosNow).toFloat / 1000000000

src/util/shell.cpp

@@ -310,7 +310,9 @@ options set_config_option(options const & opts, char const * in) {
                                   << "' cannot be set in the command line, use set_option command");
         }
     } else {
-        throw lean::exception(lean::sstream() << "invalid -D parameter, unknown configuration option '" << opt << "'");
+        // More options may be registered by imports, so we leave validating them to the Lean side.
+        // This (minor) duplication will be resolved when this file is rewritten in Lean.
+        return opts.update(opt, val.c_str());
     }
 }
 

tests/pkg/user_opt/UserOptCmdline.lean

@@ -0,0 +1,12 @@
+import UserOpt.Opts
+
+/-! Test setting user options from lakefile. -/
+
+open Lean
+
+def tst2 : MetaM Unit := do
+  assert! myBoolOpt.get (← getOptions)
+  assert! myNatOpt.get (← getOptions) == 4
+  pure ()
+
+#eval tst2

tests/pkg/user_opt/lakefile.lean

@@ -1,5 +0,0 @@
-import Lake
-open System Lake DSL
-
-package user_opt
-@[default_target] lean_lib UserOpt

tests/pkg/user_opt/lakefile.toml

@@ -0,0 +1,9 @@
+name = "user_opt"
+defaultTargets = ["UserOpt", "UserOptCmdline"]
+
+[[lean_lib]]
+name = "UserOpt"
+
+[[lean_lib]]
+name = "UserOptCmdline"
+leanOptions = { myBoolOpt = true, weak.myNatOpt = 4, weak.notMyNatOpt = 5 }