Zulip Chat Archive

Stream: general

Topic: open_locale vs open

Floris van Doorn (Sep 25 2019 at 15:32):

In #1465 we are discussing whether open_locale should be used to open namespaces (i.e. the usual open command).
This could come in various forms:

  • open_locale real also opens open real, and the same for every namespace; and/or
  • we can register namespaces, like open_namespaces nat int rat real complex in number_systems so that open_locale number_systems opens all these namespaces.

What do you think: is this a useful feature, or confusing, because now open and open_locale are not orthogonal anymore?

Reid Barton (Sep 25 2019 at 15:46):

The first one seems fine. I don't like the second one much: too hard to understand or control what is open, and a change to the open_namespaces declaration could have unknown consequences elsewhere.

Simon Hudon (Sep 25 2019 at 15:59):

That's a fair point. One downside of going that way is that we'd like setup_tactic_parser to be subsumed by open_locale and setup_tactic_parser opens a number of namespaces. We can also keep the two separate or build one on the infrastructure of the other.

Simon Hudon (Sep 25 2019 at 16:00):

One benefit of having it partially separated would be that setup_tactic_parser and open_locale tactic would have different behaviors which might be desirable.

Reid Barton (Sep 25 2019 at 16:09):

I haven't really looked into how either of these things work, but using open_locale in setup_tactic_parser looks reasonable

Reid Barton (Sep 25 2019 at 16:47):

setup_tactic_parser is so specialized that the fact that it opens namespaces doesn't bother me in the same way as if open_locale did, and so simple that it doesn't necessarily seem worth writing in terms of open_locale, in my opinion.

Last updated: Dec 20 2023 at 11:08 UTC