Panic: duplicate normalized declaration name

Stream: lean4

[Pavel Klimov]

how can I fix this?

PANIC at _private.Lean.Environment.0.Lean.AsyncConsts.add Lean.Environment:464:4: duplicate normalized declaration name parseByteArray vs. parseByteArray
backtrace:
/home/ubuntu/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean/libleanshared.so(lean_panic+0xf5) [0x7ffab85a0295]
/home/ubuntu/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean/libleanshared.so(lean_panic_fn+0x15) [0x7ffab85a0475]
/home/ubuntu/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean/libleanshared.so(l_Lean_Environment_addConstAsync+0xa72) [0x7ffab2acb182]
/home/ubuntu/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean/libleanshared.so(l_Lean_addDecl___lam__2+0x75d) [0x7ffab2a298ed]
/home/ubuntu/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean/libleanshared.so(l_Lean_addDecl+0x19bb) [0x7ffab2a2d16b]
/home/ubuntu/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean/libleanshared.so(l_Array_forIn_x27Unsafe_loop___at_____private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addSorried_spec__0+0x527) [0x7ffab3a485c7]
/home/ubuntu/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean/libleanshared.so(l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addSorried+0x44) [0x7ffab3a49894]
/home/ubuntu/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean/libleanshared.so(l_Array_forIn_x27Unsafe_loop___at___Lean_Elab_addPreDefinitions_spec__13___redArg+0x6da9) [0x7ffab3a6c0c9]
/home/ubuntu/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean/libleanshared.so(l_Lean_Elab_addPreDefinitions___lam__1+0x57e) [0x7ffab3a6db6e]
/home/ubuntu/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean/libleanshared.so(l_Lean_Elab_addPreDefinitions___lam__1___boxed+0xcc) [0x7ffab3a6e61c]
/home/ubuntu/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean/libleanshared.so(lean_apply_7+0xc0b) [0x7ffab85b586b]

It's not full log. It's just start.

[Pavel Klimov]

Renaming the function doesn't help

[Henrik Böving]

What is it that you are doing? #mwe

[Pavel Klimov]

I'm just writing normal lean code

[Pavel Klimov]

no magic

[Henrik Böving]

Please do provide a #mwe, we can't help you without seeing what you are doing

[Pavel Klimov]

oh, ok, will try :frown:

[Pavel Klimov]

While I'm trying to make mwe, I can tell you also that it also has following error:

Cannot derive parseByteArray._mutual.eq_def
  failed to generate equational theorem for 'parseByteArray._mutual'

[Pavel Klimov]

here is #mwe

set_option Elab.async false

inductive Ty
| int (width : Nat)
| struct (packed : Bool) (elementTypes : List Ty)
deriving BEq

mutual

def listOfTypesToType : List Ty → Type
| .nil => Empty
| head :: .nil => head.toType
| head :: tail => Prod head.toType (listOfTypesToType tail)

def Ty.toType : Ty → Type
| .int width => BitVec width
| .struct _ elementTypes => listOfTypesToType elementTypes

end

def typeSize : Ty → Nat
| .struct _ elementTypes => 2 + (elementTypes.map typeSize).sum
| _ => 1

theorem typeSizeGeZero : ∀ (a : Ty), (typeSize a) > 0 := by
  intro a
  cases a with
  | int _ => simp_all [typeSize]
  | struct _ elementType =>
    simp_all [typeSize]
    induction elementType with
    | nil => simp
    | cons x xs ih => omega

mutual

def structParseByteArray (packed : Bool) (types : List Ty) (data : ByteArray) (offset : Nat) :
        Except String (listOfTypesToType types) := do
  match types with
  | .nil => .error "empty struct"
  | head :: tail =>
    let alignment := if packed then 1 else 8
    let alignedOffset := (offset + alignment - 1) / alignment
    let nextOffset := alignedOffset + 8
    let currentData := data.extract alignedOffset nextOffset
    let first ← parseByteArray head currentData
    match tail with
    | .nil =>
      .ok first
    | head1 :: tail1 =>
      let second ← structParseByteArray packed (head1 :: tail1) data nextOffset
      .ok ⟨ first, second ⟩
termination_by (1 + (types.map typeSize).sum)
decreasing_by
  . simp; omega
  . simp [typeSizeGeZero]

def parseByteArray (type : Ty) (data : ByteArray) :
        Except String type.toType := do
  match type with
  | .struct packed elementTypes => structParseByteArray packed elementTypes data 0
  | t => throw s!"not implemented"
termination_by typeSize type
decreasing_by all_goals simp [typeSize]

end

[Kim Morrison]

Opening this in live.lean-lang.org does not show any errors.

[Pavel Klimov]

As far as I know, in live lean always most recent version of lean4. My code crash in v4.22.0version.

[Kim Morrison]

Then upgrade. :-)