open_locale vs open

Stream: general

[Floris van Doorn]

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]

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]

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]

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]

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

[Reid Barton]

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.