options in user attributes

Stream: general

[Floris van Doorn]

The after_set field of user attributes doesn't have access to the current options. Is it possible to change that?

open tactic
@[user_attribute] meta def my_attr : user_attribute unit unit :=
{ name := `foo,
  descr := "Test",
  after_set := some $ λ _ _ _, get_options >>= trace }

run_cmd get_options >>= trace
@[foo] def foo1 : true := trivial
set_option pp.implicit true
run_cmd get_options >>= trace
@[foo] def foo2 : true := trivial

[Floris van Doorn]

This means that for example that tracing doesn't take into account the current pp settings.

[Reid Barton]

By "have access to the current options", I guess you just mean that the options in effect at that point in the file should also be in effect when after_set runs?

[Reid Barton]

I don't know how hard this one would be, but a similar issue for simp was easy to fix:
https://github.com/leanprover-community/lean/commit/42713125a2270a07d7034abfb45af786fb5d8746

[Floris van Doorn]

Yes, that is indeed what I mean.

[Floris van Doorn]

Opening lean#546 to not forget this issue.