Zulip Chat Archive

Stream: general

Topic: options in user attributes


view this post on Zulip Floris van Doorn (Dec 25 2020 at 04:58):

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

view this post on Zulip Floris van Doorn (Dec 25 2020 at 05:00):

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

view this post on Zulip Reid Barton (Dec 25 2020 at 16:05):

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?

view this post on Zulip Reid Barton (Dec 25 2020 at 16:06):

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

view this post on Zulip Floris van Doorn (Dec 28 2020 at 20:20):

Yes, that is indeed what I mean.

view this post on Zulip Floris van Doorn (Mar 05 2021 at 04:37):

Opening lean#546 to not forget this issue.


Last updated: May 15 2021 at 23:13 UTC