Registering custom options on the command line

Stream: lean4

[Eric Wieser]

If I define a new option

register_option fooOption : Bool := {
  defValue := false
  descr := "if true, foo"
}

then while I can use this with set_option, I can't use it with lean -DfooOption=true or leanOptions := #[(`fooOption, true)] in the lakefile, as the option is processed before my file defining it is imported.

Is it possible to make this work?

[Eric Wieser]

Ah, this is lean4#3403