How does the auto-introduction of do...end block work for goto statement?

Question

The lua doc's comment on label scope:

A goto may jump to any visible label as long as it does not enter into the scope of a local variable

So in my understanding, the following code is problematic:

-- codelist 1
goto a
local x = 42
::a::

But it works well in the lua web shell. The doc continues to say:

Note that you can think of

do
  <...>
  --::a::
  goto a  -- invalid (forward jump into scope of local definition)
  goto b  -- valid (jump out of block)
  <...>
  local x
  <...>
  ::a::
  <...>
  --goto a
  ::b::
end

as equivalent to

do
  <...>
  --::a::
  goto a  -- invalid (jump into nested block prohibited because nested label not even visible here)
  goto b  -- valid (jump out of block)
  <...>
  do
    local x
    <...>
    ::a::
    <...>
    --goto a
  end
  ::b::
end

Why is ::a:: included in the auto-introduced do...end block and why isn't ::b::? Please help me understand, thanks.

Edit: I also found this old post, and it seems that there indeed was a time when codelist 1 was prohibited.

Answer 1

goto a
local x = 42
::a::

will not cause an error. Not even in 5.2

goto a
local x = 42
::a::
print("oh no")

on the other hand will.

Lua's pre-compilation will only complain if you jump into the scope of a local and acutally do something after the label while still within the local's scope. So you may jump there but you may not do something in this invalid situation.

Same with your second example. ::b:: is the end of the block. Nothing happens within the scope of x after it so it's ok to jump there.

goto b
local x = 42
::a::
print("oh no")
::b::

would be ok.