What's the deal with `open`

Stream: general

[Keeley Hoek]

namespace a

open nat
run_cmd (tactic.open_namespaces >>= tactic.trace)

end a

run_cmd (tactic.open_namespaces >>= tactic.trace)

Isn't nat supposed to be... not opened?

[Keeley Hoek]

Oh...

namespace a

open nat

def b : ℕ := 2

#check b
run_cmd (tactic.open_namespaces >>= tactic.trace)

end a

#check b
run_cmd (tactic.open_namespaces >>= tactic.trace)

gives an error at the second #check b. Did we introduce this bug, or has it always been here?

[Keeley Hoek]

Also, how could this possibly happen? The implementation of open_namespaces must be... funky

[Mario Carneiro]

What does open_namespaces even mean? Note that (at least last time I checked) open doesn't really permanently open the namespace, it just locally renames all theorems in the namespace to be usable without the namespace. If you add new theorems to the namespace they aren't "opened"

[Mario Carneiro]

which would imply that the actual state change in lean is not a list of open namespaces but rather a list of theorem aliases

[Keeley Hoek]

Woah

[Mario Carneiro]

def foo.bar := trivial

section

open foo
def foo.baz := trivial

#check bar -- ok
#check baz -- fail
end

[Keeley Hoek]

I thought it did what the doc says: Return list of currently open namespaces (the implication being that there is such a list)
Why oh why aha

[Mario Carneiro]

It is different for namespace though, I think

[Keeley Hoek]

No

[Keeley Hoek]

Wouldn't my example work then?

[Mario Carneiro]

like lean needs to know what namespace sections you are in

[Keeley Hoek]

Oh, right, I see

[Mario Carneiro]

namespace foo
namespace bar.baz

-- lean knows that I am in foo / bar.baz

end bar.baz -- or else it wouldn't be able to check that these ends are properly matched
end foo

[Keeley Hoek]

Ok well, #where has been broken in an extra way all this time... I think the current behaviour of open_namespaces is useless, so I'll file an issue

[Mario Carneiro]

I think open_namespaces is broken because there isn't actually any state change akin to close nat that it can use to remove nat from the list

[Mario Carneiro]

If you just use namespace you will see open_namespaces tracks the additions and removals correctly

[Mario Carneiro]

By the way, I think this behavior was changed in lean 4, as it is rather counterintuitive, so that open is "sticky", applying even to theorems declared after the open command. So in that case an open_namespaces list makes perfect sense

[Keeley Hoek]

Makes sense, it feels very hacky