User definable options

Stream: general

[Joe Hendrix]

Is there a way that I can set user definable options that can be parsed by tactics? I have some proofs that take a while to run, and I'd like to be able to have an option at the file or lean package level that let me configure whether they ran or not. e.g., during interactive development I disable proofs I'm not actually working on, but in a regression test they are enabled.
I noticed within a single run of the tactic monad, I can set custom option names (e.g., set_options (opt.set_bool "enable_unsafe_tac" tt)), but the value doesn't appear to show up in tactics farther down the file. The set_option command also doesn't allow custom options.

[Sebastian Ullrich]

set_option accepts only built-in options, but using the set_options primitive should work. Did you execute that code in a run_command?

[Joe Hendrix]

Sorry for the delay; I didn't see this until today. Here's a sample script:

open tactic

meta
def get_my_opt : tactic unit := do
  o ← get_options,
  trace (repr (o.get_bool "foo" ff))

meta
def set_my_opt : tactic unit := do
  o ← get_options,
  set_options (o.set_bool "foo" tt),
  get_my_opt

run_cmd get_my_opt
run_cmd set_my_opt
run_cmd get_my_opt

The output I get is:

ff
tt
ff

So set_options works in the current command, but the option is forgotten in subsequent commands.

[Sebastian Ullrich]

Ah, that's too bad. You may want to fake the option with a custom attribute (which can be set globally or locally, but unset only locally). I'm not aware of a better solution.

[Joe Hendrix]

Thanks, that seems to work well.

[Mario Carneiro]

Is this improving in lean 4? More generally, it would be nice if there was a way to persist arbitrary data across different commands. Does everything have to go via adding defs to the environment?

[Joe Hendrix]

I could see use cases for persisting data, but I also think it's important that tactics could be run concurrently, and the results cached. Given that goal, set_options behavior doesn't seem to surprising.
In Haskell, you can define package level options and use them to define constants that can be checked at compile time (via CPP). That's what I was hoping for here, so I could pass a flag to build or configure that controlled whether an axiom was allowed to be used. The attribute trick doesn't seem too bad though.