Error when executing files with Mathlib import

Stream: mathlib4

[Amos Nicodemus]

I am sure whether this is the correct place to ask, so please correct me if I am wrong.
When I try to execute the following code in my lean project, I get the error "INTERNAL PANIC: unreachable code has been reached":

import Mathlib.Data.Finset.Defs

def main : IO Unit :=
  IO.println "Hello world"

Everything works if I remove the line "import Mathlib.Data.Finset.Defs" or if I replace it by "import Mathlib.Init". I am working with lean version "v4.26.0-rc2". As far as I can tell this is a bug in Lean or Mathlib, is this correct?

[Aaron Liu]

doesn't seem to panic when I do this in the web editor

[Amos Nicodemus]

Is there a way to execute a file in the web editor? Because the problem is not building the file/project, or working with lean in the editor (this works fine), but executing it (using lake exe).

[Kevin Buzzard]

If you want to investigate further yourself then one way of course is to keep replacing a file with its imports, deleting imports when there is more than one etc etc

[Kevin Buzzard]

When you've found the offending file, cut and paste it in and then start deleting code from the file starting at the bottom and eventually you'll find your culprit

[Amos Nicodemus]

The problem seems to be with "Mathlib.Data.List.Defs", when I import it and try to execute the file, then it does not work, but when I import all its imports then it does work. When I copy paste the file (and remove the module and public declarations, as this otherwise gives error in the editor), then everything runs. So I'm not sure what is exactly wrong here...

[Amos Nicodemus]

Can someone maybe check whether it works for them or whether this is a general issue?
And could this be related to this issue?

[Julian Berman]

Did you try the second half of Kevin's suggestion? Once you have a file which causes this, which it sounds like you do, you can start to minimize what within it causes this and use that to create a minimal reproducer of the issue.

[Amos Nicodemus]

I pasted the whole file, and then I worked (when removing the public and module keywords). But when I imported the same file, it did not work.

[Amos Nicodemus]

So as far as I can tell it is not a specific definition/lemma alone which breaks it

[Julian Berman]

Here is a bit more minimizing, I created a project with just your main function and a single file which replicates the import you found, then deleted stuff from the end while preserving the error (so hopefully I haven't overminimized). I ended up with a file with:

module

public import Mathlib.Util.CompileInductive

namespace List

variable (p : α → Prop) [DecidablePred p] (l : List α)

/-- Given a decidable predicate `p` and a proof of existence of `a ∈ l` such that `p a`,
choose the first element with this property. This version returns both `a` and proofs
of `a ∈ l` and `p a`. -/
def chooseX : ∀ l : List α, ∀ _ : ∃ a, a ∈ l ∧ p a, { a // a ∈ l ∧ p a }
  | [], hp => False.elim (Exists.elim hp fun _ h => not_mem_nil h.left)
  | l :: ls, hp =>
    if pl : p l then ⟨l, ⟨mem_cons.mpr <| Or.inl rfl, pl⟩⟩
    else
      -- pattern matching on `hx` too makes this not reducible!
      let ⟨a, ha⟩ :=
        chooseX ls
          (hp.imp fun _ ⟨o, h₂⟩ => ⟨(mem_cons.mp o).resolve_left fun e => pl <| e ▸ h₂, h₂⟩)
      ⟨a, mem_cons.mpr <| Or.inr ha.1, ha.2⟩

Now you can keep going probably by inlining that one remaining import file and continuing to delete.

[Julian Berman]

I couldn't resist a bit more, so here, now there's two files (the above, and now the below) and this is free of Mathlib:

module

public meta import Lean.Elab.Command
public meta import Lean.Compiler.CSimpAttr

public meta section

open Lean Meta

private def replaceConst (repl : AssocList Name Name) (e : Expr) : Expr :=
  e.replace fun | .const n us => repl.find? n |>.map (.const · us) | _ => none

/-- Returns the names of the recursors for a nested or mutual inductive,
using the `all` and `numMotives` arguments from `RecursorVal`. -/
def mkRecNames (all : List Name) (numMotives : Nat) : List Name :=
  if numMotives ≤ all.length then
    all.map mkRecName
  else
    let main := all[0]!
    all.map mkRecName ++
      (List.range (numMotives - all.length)).map (fun i => main.str s!"rec_{i+1}")

private def addAndCompile' (decl : Declaration) : CoreM Unit := do
  try addAndCompile decl
  catch e =>
    match decl with
    | .defnDecl val => throwError "while compiling {val.name}: {e.toMessageData}"
    | .mutualDefnDecl val => throwError "while compiling {val.map (·.name)}: {e.toMessageData}"
    | _ => unreachable!

/--
Compile the definition `dv` by adding a second definition `dv✝` with the same body,
and registering a `csimp`-lemma `dv = dv✝`.
-/
def compileDefn (dv : DefinitionVal) : MetaM Unit := do
  if ((← getEnv).getModuleIdxFor? dv.name).isNone then
    -- If it's in the same module then we can safely just call `compileDecl`
    -- on the original definition
    return ← compileDecl <| .defnDecl dv
  let name ← mkFreshUserName dv.name
  addAndCompile' <| .defnDecl { dv with name }
  let levels := dv.levelParams.map .param
  let old := .const dv.name levels
  let new := .const name levels
  let name ← mkFreshUserName <| dv.name.str "eq"
  addDecl <| .thmDecl {
    name
    levelParams := dv.levelParams
    type := ← mkEq old new
    value := ← mkEqRefl old
  }
  Compiler.CSimp.add name .global

open Elab

/-- Returns true if the given declaration has a `@[csimp]` lemma. -/
def hasCSimpLemma (env : Environment) (n : Name) : Bool :=
  (Compiler.CSimp.ext.getState env).map.contains n

/--
Generate compiled code for the recursor for `iv`, excluding the `sizeOf` function.
-/
def compileInductiveOnly (iv : InductiveVal) (rv : RecursorVal) (warn := true) : MetaM Unit := do
  if ← isProp rv.type then
    if warn then logWarning m!"not compiling {rv.name}"
    return
  let levels := rv.levelParams.map .param
  let rvs ←
    if rv.numMotives == 1 then pure [rv]
    else mkRecNames iv.all rv.numMotives |>.mapM getConstInfoRec
  let rvs ← rvs.mapM fun rv => return (rv, ← mkFreshUserName rv.name)
  let repl := rvs.foldl (fun l (rv, name) => .cons rv.name name l) .nil
  addAndCompile' <| .mutualDefnDecl <|← rvs.mapM fun (rv, name) => do
    pure { rv with
      name
      value := ← forallTelescope rv.type fun xs body => do
        let major := xs[rv.getMajorIdx]!
        (← whnfD <| ← inferType major).withApp fun head args => do
          let .const iv levels' := head | throwError "not an inductive"
          let iv ← getConstInfoInduct iv
          let rv' ← getConstInfoRec <| mkRecName iv.name
          if !iv.isRec && rv'.numMotives == 1 && iv.numCtors == 1 && iv.numIndices == 0 then
            let rule := rv.rules[0]!
            let val := .beta (replaceConst repl rule.rhs) xs[:rv.getFirstIndexIdx]
            let val := .beta val ⟨.map (major.proj iv.name) <| .range rule.nfields⟩
            mkLambdaFVars xs val
          else
            let val := .const (mkCasesOnName iv.name) (.param rv.levelParams.head! :: levels')
            let val := mkAppN val args[:rv'.numParams]
            let val := .app val <| ← mkLambdaFVars xs[rv.getFirstIndexIdx:] body
            let val := mkAppN val xs[rv.getFirstIndexIdx:]
            let val := mkAppN val <| rv.rules.toArray.map fun rule =>
              .beta (replaceConst repl rule.rhs) xs[:rv.getFirstIndexIdx]
            mkLambdaFVars xs val
      hints := .opaque
      safety := .partial
    }
  for (rv, name) in rvs do
    let old := .const rv.name levels
    let new := .const name levels
    let name ← mkFreshUserName <| rv.name.str "eq"
    addDecl <| .mutualDefnDecl [{
      name
      levelParams := rv.levelParams
      type := ← mkEq old new
      value := .const name levels
      hints := .opaque
      safety := .partial
    }]
    Compiler.CSimp.add name .global
  for name in iv.all do
    for aux in [mkRecOnName name, (mkBRecOnName name).str "go", mkBRecOnName name] do
      if let some (.defnInfo dv) := (← getEnv).find? aux then
        compileDefn dv

mutual

/--
Generate compiled code for the recursor for `iv`.
-/
partial def compileInductive (iv : InductiveVal) (warn := true) : MetaM Unit := do
  let rv ← getConstInfoRec <| mkRecName iv.name
  if hasCSimpLemma (← getEnv) rv.name then
    if warn then logWarning m!"already compiled {rv.name}"
    return
  compileInductiveOnly iv rv warn
  compileSizeOf iv rv

/--
Compiles the `sizeOf` auxiliary functions. It also recursively compiles any inductives required to
compile the `sizeOf` definition (because `sizeOf` definitions depend on `T.rec`).
-/
partial def compileSizeOf (iv : InductiveVal) (rv : RecursorVal) : MetaM Unit := do
  let go aux := do
    if let some (.defnInfo dv) := (← getEnv).find? aux then
      if !hasCSimpLemma (← getEnv) aux then
        let deps : NameSet := dv.value.foldConsts ∅ fun c arr =>
          if let .str name "_sizeOf_inst" := c then arr.insert name else arr
        for i in deps do
          -- We only want to recompile inductives defined in external modules, because attempting
          -- to recompile `sizeOf` functions defined in the current module multiple times will lead
          -- to errors. An entire mutual block of inductives is compiled when compiling any
          -- inductive within it, so every inductive within the same module can be explicitly
          -- compiled using `compile_inductive%` if necessary.
          if ((← getEnv).getModuleIdxFor? i).isSome then
            if let some (.inductInfo iv) := (← getEnv).find? i then
               compileInductive iv (warn := false)
        compileDefn dv
  for name in iv.all do
    for i in [:rv.numMotives] do
      go <| name.str s!"_sizeOf_{i+1}"
    go <| name.str "_sizeOf_inst"

end

/--
`compile_inductive% Foo` creates compiled code for the recursor `Foo.rec`,
so that `Foo.rec` can be used in a definition
without having to mark the definition as `noncomputable`.
-/
elab tk:"compile_inductive% " i:ident : command => Command.liftTermElabM do
  let n ← realizeGlobalConstNoOverloadWithInfo i
  let iv ← withRef i <| getConstInfoInduct n
  withRef tk <| compileInductive iv

compile_inductive% False

[Julian Berman]

Possibly that still can be minimized a bit but if it's free of Mathlib you can essentially file a bug.

[Julian Berman]

(n.b. there's one visible unreachable! in that file -- but if I change it to throwError it doesn't seem that that's the one being hit.)

[Malvin Gattinger]

Fyi, the original problem seems to not happen with Lean and mathlib version v4.25.2.

[Henrik Böving]

This issue occurs due to two factors. The first is the module system that changed the behavior of the inliner for, so far, unknown reasons. However, the behavior of compile_inductive% on False has always been wrong to begin with and so far merely been fixed by the inliner by chance. First things first, it is unnecessary to even compile_inductive% False because False.rec is the single recursor that the compiler has native support for. The reason that calling compile_inductive% on it causes an issue, is that it introduces a new constant False.rec' = unreach. This constant used to be inlined but with the new module system does not get inlined for some reason. Because of this, the compiler decides to closed term lift it and we end up executing an unreachable during initialization. This behavior is a known limitation/bug of the current closed term extraction feature.

The correct fix would be for mathlib to either stop calling compile_inductive% on False as it is actively harming compiler optimizations and unnecessary or to at least place a @[no_extract] attribute on the False.rec' that compile_inductive% generates. This attribute informs the closed term extractor that it is not supposed to pull the constant out and is also placed on other always crashing symbols like panic! or unreachable!.

[Ruben Van de Velde]

#32225