Broken compilation

Stream: lean4

[Arthur Paulino]

Hi! I'm facing a weird issue with compiled Lean 4 code.

If you clone https://github.com/yatima-inc/Vero and go to Tests/Reduce.lean and place a #eval main at the end of the file you will see that it runs just fine.

But if, instead, you do lake build Tests.Reduce and then run ./build/bin/Tests-Reduce, this happens:

~/dev/lean/Vero λ ./build/bin/Tests-Reduce
INTERNAL PANIC: executed 'sorry'

I've never seen this happen before. Any idea what might be happening here? Thanks in advance!

[Sebastian Ullrich]

Could you run it under gdb and break on lean_internal_panic?

[Sebastian Ullrich]

I suppose we could print a backtrace on internal panics as well

[Arthur Paulino]

Sebastian Ullrich said:

Could you run it under gdb and break on lean_internal_panic?

How do I do that? Is it a lake command?

[Sebastian Ullrich]

gdb ./build/bin/Tests-Reduce then b lean_internal_panic, run, bt (from memory)

[Arthur Paulino]

(gdb) b lean_internal_panic
Ponto de parada 1 at 0x2f527c0
(gdb) run
Starting program: /home/arthur/dev/lean/Vero/build/bin/Tests-Reduce
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

Breakpoint 1, 0x00005555584a67c0 in lean_internal_panic ()
(gdb) bt
#0  0x00005555584a67c0 in lean_internal_panic ()
#1  0x00005555584a69ad in lean_sorry ()
#2  0x0000555555a79477 in initialize_Vero_Syntax_Core_Data ()
#3  0x0000555555a3f688 in initialize_Tests_Reduce ()
#4  0x0000555555a405bc in main ()

[Sebastian Ullrich]

Ah, that is an unfortunate limitation of the current compiler. You should not use sorry in constants (parameterless defs) like in https://github.com/yatima-inc/Vero/blob/main/Vero/Syntax/Core/Data.lean#L18.

[Arthur Paulino]

Alright, good to know. Thanks again!

[Arthur Paulino]

Hi! I hit some strange panic again on this branch: https://github.com/yatima-inc/yatima-lang/tree/ap/transpiler-deepdive-pt2

This is the output of gdb:

Breakpoint 1, 0x000055555945f400 in lean_internal_panic ()
(gdb) bt
#0  0x000055555945f400 in lean_internal_panic ()
#1  0x000055555945f47d in lean_internal_panic_unreachable ()
#2  0x0000555556b25705 in initialize_Yatima_Transpiler2_Transpiler ()
#3  0x0000555556b41d30 in initialize_Yatima_Cli_TranspileCmd ()
#4  0x0000555556081860 in initialize_Main ()
#5  0x0000555556081e08 in main ()

The strangeness is that there's no unreachable! in my code. The error happens when I plug this file on my import tree: https://github.com/yatima-inc/yatima-lang/blob/ap/transpiler-deepdive-pt2/Yatima/Transpiler2/Transpiler.lean

[Arthur Paulino]

Is there something I can do to avoid that unreachable panic on the "initialize" routine?

[Arthur Paulino]

Another clue... the code worked just fine with the previous version of that file: https://github.com/yatima-inc/yatima-lang/blob/ap/transpiler-deepdive-pt2/Yatima/Transpiler/Transpiler.lean

In fact, as soon as I plug that one instead, it works like magic

[Henrik Böving]

If you compile with debugging options and without C optimizaitons enabld you get:

#0  0x0000555559c45200 in lean_internal_panic ()
#1  0x0000555559c4527d in lean_internal_panic_unreachable ()
#2  0x0000555557304bd0 in _init_l_Yatima_Transpiler_appendCtor___closed__5 () at ./build/ir/Yatima/Transpiler2/Transpiler.c:2371
#3  0x0000555557303046 in initialize_Yatima_Transpiler2_Transpiler (builtin=1 '\001', w=0x1) at ./build/ir/Yatima/Transpiler2/Transpiler.c:29695
#4  0x0000555557321c64 in initialize_Yatima_Cli_TranspileCmd (builtin=1 '\001', w=0x1) at ./build/ir/Yatima/Cli/TranspileCmd.c:1337
#5  0x000055555609ae94 in initialize_Main (builtin=1 '\001', w=0x1) at ./build/ir/Main.c:550
#6  0x000055555609b3f6 in main (argc=1, argv=0x7fffffffd7b8) at ./build/ir/Main.c:636
(gdb) up
#1  0x0000555559c4527d in lean_internal_panic_unreachable ()
(gdb)
#2  0x0000555557304bd0 in _init_l_Yatima_Transpiler_appendCtor___closed__5 () at ./build/ir/Yatima/Transpiler2/Transpiler.c:2371
list
2371    lean_internal_panic_unreachable();
(gdb) list
2366    }
2367    }
2368    static lean_object* _init_l_Yatima_Transpiler_appendCtor___closed__5() {
2369    _start:
2370    {
2371    lean_internal_panic_unreachable();
2372    }
2373    }
2374    static lean_object* _init_l_Yatima_Transpiler_appendCtor___closed__6() {
2375    _start:
(gdb)

so apparently it came to the conclusion, that there in your appendCtor function it is appropriate to have an unreachable somewhere. Looking at the output of the ir with: set_option trace.compiler.ir.result true in on your function (specifically searched for the closed_5 term there) it appears this unreachable pops up when you walk into a case arm " Yatima.Split.injᵣ →" which I don't see explicitly getting mentioned in this function so its either getting inlined from somewhere or the macro stuff you got going on there is producing it.

@Arthur Paulino

[Arthur Paulino]

Hmm, I don't see it :dizzy:

[Henrik Böving]

It could also be that the compiler decided to optimize something you generated there into an unreachable.

[Henrik Böving]

Hm no, the new compiler also already seems to believe that there is an unreachable here, right from the beginning.

[Arthur Paulino]

But it doesn't even reach that code. If you go to Main.lean and print something there, it doesn't show

[Henrik Böving]

That's not necessarily an issue, as you can see in the backtrace it is already panicking this way during initialization phase so before it ever reaches main during setting up the initial environment. It appears you are setting up something here in the Transpiler2 that calls into this code which in turn calls into appendCtor an panics. Looking at the generate code for appendCtor it does also seem to believe that it should indeed make the injr unreachable:

def Yatima.Transpiler.appendCtor : Both Constructor → AST → Nat → TranspileM Unit :=
fun ctor indLit indices => do
  let type ← derefExpr { anon := ctor.anon.type, meta := ctor.meta.type }
  let name : Name := Split.projᵣ ctor.meta.name
  let idx : Nat := Split.projₗ ctor.anon.idx
  let __do_lift ← read
  match Store.telescopeLamPi __do_lift.store #[] type with
    | some (#[], snd) =>
      appendBinding
        (name,
          cons (sym "CONS")
            (cons (toAST indLit)
              (cons
                (cons (sym "CONS")
                  (cons
                    (toAST
                      (match ctor.anon.idx with
                      | Split.injₗ a => a))
                    (cons (sym "NIL") nil)))
                nil)))
        true

And the specific piece of code that is at fault here is if you look back at the original source this one:

          cons (sym "CONS")
            (cons (toAST indLit)
              (cons
                (cons (sym "CONS")
                  (cons
                    (toAST
                      (match ctor.anon.idx with
                      | Split.injₗ a => a))
                    (cons (sym "NIL") nil)))
                nil)))

which is the one coming from your macro so I'd claim the macro is at fault for putting an unreachable where there is reachable code.

Note: the other calls to your macro code are also doing similar stuff with only matching on one variant so I'm not 100% sure it is actually this macro, figuring out which macro call is actually at fault here would take some more time.

[Arthur Paulino]

We have had issues with antiquotations before. Maybe it's something similar. I'll try to replace those after dinner

[Arthur Paulino]

Thanks for the support!!

[Arthur Paulino]

Wait, that is not the issue. The other arm of the match is indeed unreachable

[Arthur Paulino]

Yeah, I just commented out the code of appendCtor and it hit the same problem. I think I'm just doing something forbidden with the current compiler, like the previous time when I had constants with sorry, which was causing an internal panic even though the sorrys were never actually met during execution