custom options

Stream: general

[Heather Macbeth]

I noticed that in Lean 4 you can make your own options with register_option:
https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/md/extra/options.md#making-our-own

Does this feature exist in Lean 3?

[Alex J. Best]

Unfortunately not. I think the closet thing you can do is register a tracing option. Which in the past people have (ab)used to pretend it's like a normal option

[Heather Macbeth]

I'd be up for that abuse, do you know of an example I could look at?

[Alex J. Best]

I'm on mobile, but i found the thread I'm thinking of https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/A.20useless.20option.20which.20I.20can.20use.20for.20another.20purpose.3F

[Alex J. Best]

I can look a bit later for something more specific

[Heather Macbeth]

Thanks! I see that I can register my fake tracing option using declare_trace; I think the only other thing I need to know is how to access the state of the option within meta code.

[Kyle Miller]

Here's another reference I found: https://leanprover.zulipchat.com/#narrow/stream/303200-sphere-eversion/topic/Chapter.203.20coordination/near/296282435 (it uses the declare_trace hack)

[Kyle Miller]

I believe the function is docs#tactic.get_bool_option

[Heather Macbeth]

Thanks @Alex J. Best @Kyle Miller, I got it working! See #16586 for my use case.

[Kevin Buzzard]

Nice work!