Unreachable code reached with `precompileModules`

chrisflav commented 7 months ago

Prerequisites

[X] Put an X between the brackets on this line if you have done all of the following:
- Check that your issue is not already filed.
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

When compiling the project with lake build, this error message is thrown:

[3/5] Building Main error: > LEAN_PATH=./.lake/build/lib LD_LIBRARY_PATH=./.lake/build/lib /home/christian/.elan/toolchains/leanprover--lean4---stable/bin/lean ./././Main.lean -R ././. -o ./.lake/build/lib/Main.olean -i ./.lake/build/lib/Main.ilean -c ./.lake/build/ir/Main.c --load-dynlib=./.lake/build/lib/libUnreachable-Fails-1.so error: stderr: INTERNAL PANIC: unreachable code has been reached error: external command /home/christian/.elan/toolchains/leanprover--lean4---stable/bin/lean exited with code 1

Context

I was playing around with the FFI and in src/lake/examples/ffi/lib/lakefile.lean the option precompileModules := true was suggested.

Steps to Reproduce

This is the project structure:


.
├── lakefile.lean
├── lake-manifest.json
├── lean-toolchain
├── Main.lean
└── Unreachable
└── Fails.lean

2 directories, 5 files

2. This is `lakefile.lean`:
```lean
import Lake
open System Lake DSL

package unreachable {
  /- Setting this to `false` this makes it work -/
  precompileModules := true
}

lean_lib Unreachable

@[default_target] lean_exe test {
  root := `Main
}

This is Main.lean
```
import Unreachable.Fails
```

def main : IO Unit := do IO.println "hi"

4. This is `Unreachable/Fails.lean`
```lean
inductive World where
  | elementary
  | composed

/- Dropping the elementary constructor makes it work.-/
inductive EType : World → Type where
  | elementary : EType .elementary
  | composed (name : String) : EType .composed

def Composed : Type := EType .composed

/- Changing this to `def` makes it work. -/
abbrev Composed.name (s : Composed) : String :=
  match s with
  | .composed name => name

/- Dropping this line makes it work. -/
def Composed.toString (c : Composed) : String :=
  s!"column {c.name}"

Expected behavior: lake build succeeds.

Actual behavior: lake build crashes.

Versions

Lean version: 4.5.0 OS version: Debian GNU/Linux 12 (bookworm)

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

semorrison commented 7 months ago

This is not necessarily actually a lake bug, but I'm guessing the @tydeu is going to be the best person to diagnose this.

tydeu commented 7 months ago

@semorrison While this is not a Lake problem, I was (to my surprise) able to discover the source of the error. Setting trace.compiler.ir.result true on Composed.toString show the following IR result:

[result]
def Composed.toString._closed_1 : obj :=
  let x_1 : obj := "column ";
  ret x_1
def Composed.toString._closed_2 : obj :=
  ⊥
def Composed.toString._closed_3 : obj :=
  let x_1 : obj := "";
  ret x_1
def Composed.toString._closed_4 : obj :=
  let x_1 : obj := Composed.toString._closed_2;
  let x_2 : obj := Composed.toString._closed_3;
  let x_3 : obj := String.append x_1 x_2;
  dec x_2;
  ret x_3
def Composed.toString (x_1 : @& obj) : obj :=
  case x_1 : obj of
  EType.elementary →
    let x_2 : obj := Composed.toString._closed_4;
    ret x_2
  EType.composed →
    let x_3 : obj := proj[0] x_1;
    let x_4 : obj := Composed.toString._closed_1;
    let x_5 : obj := String.append x_4 x_3;
    let x_6 : obj := Composed.toString._closed_3;
    let x_7 : obj := String.append x_5 x_6;
    dec x_6;
    ret x_7
def Composed.toString._boxed (x_1 : obj) : obj :=
  let x_2 : obj := Composed.toString x_1;
  dec x_1;
  ret x_2

The are a number of problems with this IR (e.g., there should not be an elementary case), but the one directly producing the panic is that Composed.toString._closed_2 is defined as ⊥ (unreachable) and Lean compiles and initializes all closed terms. This means its compiled C initializer is:

static lean_object* _init_l_Composed_toString___closed__2() {
_start:
{
lean_internal_panic_unreachable();
}
}

which is run during module initialization like so:

LEAN_EXPORT lean_object* initialize_Lakepen_Unreachable(uint8_t builtin, lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_World_noConfusion___rarg___closed__1 = _init_l_World_noConfusion___rarg___closed__1();
lean_mark_persistent(l_World_noConfusion___rarg___closed__1);
l_Composed_toString___closed__1 = _init_l_Composed_toString___closed__1();
lean_mark_persistent(l_Composed_toString___closed__1);
l_Composed_toString___closed__2 = _init_l_Composed_toString___closed__2();
lean_mark_persistent(l_Composed_toString___closed__2);
l_Composed_toString___closed__3 = _init_l_Composed_toString___closed__3();
lean_mark_persistent(l_Composed_toString___closed__3);
l_Composed_toString___closed__4 = _init_l_Composed_toString___closed__4();
lean_mark_persistent(l_Composed_toString___closed__4);
return lean_io_result_mk_ok(lean_box(0));
}

Ironically, it is actually good that lake build is erroring here as an executable importing this module would fail with the panic as well even if it were not precompiled (as the main function also calls the initializers).

The bad news, though, is that this is compiler error, and unless this is just a minor oversight somewhere this will likely need to wait on the new compiler to fix it. @hargoniX, as you one of the experts on the Lean compiler, do you know if this something that can be fixed relatively easily?

Kha commented 7 months ago

Essentially this is #467

leanprover / lean4