Topic: User definable options
Joe Hendrix (Jan 11 2019 at 23:23):
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 (Jan 12 2019 at 12:46):
set_option accepts only built-in options, but using the
set_options primitive should work. Did you execute that code in a
Joe Hendrix (Jan 22 2019 at 21:06):
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
set_options works in the current command, but the option is forgotten in subsequent commands.
Sebastian Ullrich (Jan 22 2019 at 21:39):
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 (Jan 22 2019 at 21:57):
Thanks, that seems to work well.
Mario Carneiro (Jan 22 2019 at 22:08):
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 (Jan 23 2019 at 05:42):
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.
Last updated: May 16 2021 at 05:21 UTC