Zulip Chat Archive

Stream: general

Topic: What's the deal with `open`


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Keeley Hoek (Apr 21 2020 at 07:11):

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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Keeley Hoek (Apr 21 2020 at 07:14):

Woah

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 07:16):

It is different for namespace though, I think

view this post on Zulip Keeley Hoek (Apr 21 2020 at 07:16):

No

view this post on Zulip Keeley Hoek (Apr 21 2020 at 07:16):

Wouldn't my example work then?

view this post on Zulip Mario Carneiro (Apr 21 2020 at 07:17):

like lean needs to know what namespace sections you are in

view this post on Zulip Keeley Hoek (Apr 21 2020 at 07:17):

Oh, right, I see

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 07:21):

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

view this post on Zulip 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

view this post on Zulip Keeley Hoek (Apr 21 2020 at 07:54):

Makes sense, it feels very hacky


Last updated: May 14 2021 at 12:18 UTC