setOptionFromString semantics

Stream: lean4

[Leni Aniva]

There's this function in Lean/Data/Options.lean:

def setOptionFromString (opts : Options) (entry : String) : IO Options := do
  let ps := (entry.splitOn "=").map String.trim
  let [key, val] ← pure ps | throw $ IO.userError "invalid configuration option entry, it must be of the form '<key> = <value>'"
  let key := Name.mkSimple key
  let defValue ← getOptionDefaultValue key
  match defValue with
  | DataValue.ofString _ => pure $ opts.setString key val
  | DataValue.ofBool _   =>
    if key == `true then pure $ opts.setBool key true
    else if key == `false then pure $ opts.setBool key false
    else throw $ IO.userError s!"invalid Bool option value '{val}'"
  | DataValue.ofName _   => pure $ opts.setName key val.toName
  | DataValue.ofNat _    =>
    match val.toNat? with
    | none   => throw (IO.userError s!"invalid Nat option value '{val}'")
    | some v => pure $ opts.setNat key v
  | DataValue.ofInt _    =>
    match val.toInt? with
    | none   => throw (IO.userError s!"invalid Int option value '{val}'")
    | some v => pure $ opts.setInt key v
  | DataValue.ofSyntax _ => throw (IO.userError s!"invalid Syntax option value")

I found this function to be a bit counterintuitive since

1. The name should be something like Name.str (Name.str ... name1) name2" instead of Name.mkSimple`
2. The boolean parsing is completely wrong since key is the name of the key and should never be true or false
   I can make a PR for this if this semantics makes more sense

[Mario Carneiro]

You are right, those both look like bugs. Is this function used at all? Removing it might be the more appropriate response.

[Leni Aniva]

Mario Carneiro said:

You are right, those both look like bugs. Is this function used at all? Removing it might be the more appropriate response.

Its not used anywhere in lean, but would be pretty handy had it been written correctly

[Mario Carneiro]

that sounds like a better fit for std