Stream: general

Topic: What's the deal with open

Keeley Hoek (Apr 21 2020 at 07:10):

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 (Apr 21 2020 at 07:10):

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 (Apr 21 2020 at 07:11):

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

Mario Carneiro (Apr 21 2020 at 07:12):

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 (Apr 21 2020 at 07:13):

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

Woah

Mario Carneiro (Apr 21 2020 at 07:14):

def foo.bar := trivial

section

open foo
def foo.baz := trivial

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


Keeley Hoek (Apr 21 2020 at 07:15):

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 (Apr 21 2020 at 07:16):

It is different for namespace though, I think

No

Keeley Hoek (Apr 21 2020 at 07:16):

Wouldn't my example work then?

Mario Carneiro (Apr 21 2020 at 07:17):

like lean needs to know what namespace sections you are in

Oh, right, I see

Mario Carneiro (Apr 21 2020 at 07:17):

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 (Apr 21 2020 at 07:18):

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 (Apr 21 2020 at 07:20):

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 (Apr 21 2020 at 07:21):

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

Mario Carneiro (Apr 21 2020 at 07:24):

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 (Apr 21 2020 at 07:54):

Makes sense, it feels very hacky

Last updated: May 14 2021 at 12:18 UTC