no need to close namespace

Stream: lean4

[Kevin Buzzard]

I ran into an issue today which I was getting very confused about, and then it transpired that I hadn't closed a namespace and lean had failed to add the final definition in a file into the system. I cannot reproduce right now, annoyingly, but I can observe that

namespace foo

compiles. Is this expected? In Lean 3 this didn't work.

[Gabriel Ebner]

I really like this new feature.

[Kevin Buzzard]

It could be the case that the error I thought was caused by not closing a namespace was instead caused by me not typing leanpkg build and then restarting Lean. I find the current behaviour quite counterintuitive when I am working on files A and B, with B importing A and me adding lemmas to both. In short, the namespace thing might be a red herring and it's just me not quite used to the new system.

[Marcus Rossel]

Just for documentation purposes: I just ran into the same issue and was super confused at first.

[Arthur Paulino]

Same here