Running lean -D my_option=false

Stream: lean4

[Tomas Skrivan]

If I register an option with

register_option my_option : Bool :=  {
  defValue := true
  group    := ""
  descr    := ""
}

Can I run lean -D my_option=false ...? Or do I need to register my_option in a different way?

I'm getting an error

invalid -D parameter, unknown configuration option 'my_option'

[Mario Carneiro]

I have heard this issue before, I don't think there is a fix yet. Probably you should open an issue

[Mario Carneiro]

for lean code we have sudo set_option thanks to @Gabriel Ebner but I don't think there is a -D equivalent

[Gabriel Ebner]

I think the only way would be to declare the option in a plugin.

[Tomas Skrivan]

Hmm, maybe this all is an XY problem.

What I want is to have a command #profile_this_file that reruns the file with profiler settings and somehow processes the output. The issue is that the command #profile_this_file needs to be disabled when rerunning the file with profiler on, otherwise it gets into an infinite loop.

I thought I might use options to do that. Any idea how could I achieve that?

[Kyle Miller]

If the command is running its own frontend (where it loads the file, parses imports, then elaborates all commands), you could inject an extra import that defines a new elaborator that overrides the #profile_this_file command to be a no-op

[Tomas Skrivan]

Good idea, a bit hacky but doable.

Right now the command just runs lake env lean ... file.lean

[Gabriel Ebner]

Another hacky but easy solution would be to set an environment variable.

[Scott Morrison]

There is a tempting looking (opts : Options) argument to processHeader, which one might hope lets you set options when you are running your own frontend. I can't immediately work out where that argument feeds into, however.