what happened upgrading from lean4:v4.21.0 to lean4:v4.22.0

Stream: general

[Luc Duponcheel]

Hello, I know that, by defining my the unsafe parallelFibonacci I am "driving on the dangerous fast lane", but, in one way or another, by upgrading from lean4:v4.21.0 to lean4:v4.22.0, my #eval tasksSpawningFibonacci 24, using Task, does not work any more. Note that in the attached video, 2^25 threads are spawned, which takes some time, but #eval tasksSpawningFibonacci 5, also crashes with lean4:v4.22.0, so, I think it is not a stack size issue.

simplescreenrecorder-2025-09-08_22.48.30.mkv

[Henrik Böving]

Nothing in particular comes to mind, you'll have to provide a #mwe.

[Luc Duponcheel]

Henrik,

uncomment the #eval when viewing it in the Lean playground

you can also copy/paste (or download attachment) and run it locally with version 21

Code listing

class Functional
    (program : Type → Type → Type) where
  asProgram {α β : Type} :
    (α → β) → program α β

export Functional (asProgram)

class Functorial
    (program : Type → Type → Type) where
  andThenF {α β γ : Type} :
    program α β → (β → γ) → program α γ

export Functorial (andThenF)

infixl:50 " >-> " => andThenF

class Sequential
    (program : Type → Type → Type) where
  andThenP {α β γ : Type} :
    program α β → program β γ → program α γ

export Sequential (andThenP)

infixl:50 " >=> " => andThenP

class Creational
    (program : Type → Type → Type) where
  productSeq {α β γ : Type} :
    program α β → program α γ → program α (β × γ)

export Creational (productSeq)

infixl:60 " &&& " => productSeq

class Conditional
    (program : Type → Type → Type) where
  sum {α β γ : Type} :
    program γ α → program β α → program (γ ⊕ β) α

export Conditional (sum)

infixl:55 " ||| " => sum

class Parallel (program : Type → Type → Type) where
  bothPar {α β γ δ : Type} :
  program α γ → program β δ → program (α × β) (γ × δ)

export Parallel (bothPar)

infixl:60 " |&| " => bothPar

def identity
    [Functional program] :
  program α α :=
    asProgram λ α => α

def let_
    [Functional program]
    [Sequential program]
    [Creational program] :
  program α β → program (α × β) γ → program α γ :=
    λ αpβ αaβpγ => identity &&& αpβ >=> αaβpγ

 def if_
    [Functional program]
    [Sequential program]
    [Creational program]
    [Conditional program] :
  program α Bool →
  program α β →
  program α β →
  program α β :=
    λ αpb t_apβ f_apβ =>
      let_ αpb $
        asProgram (
          λ αab => match αab with
            | ⟨α, true⟩ => .inl α
            | ⟨α, false⟩ => .inr α
        ) >=>
        t_apβ ||| f_apβ

def dup
    [Functional program] :
  program α (α × α) :=
    asProgram λ α => (α, α)

def productPar {α β γ : Type}
    [Functional program]
    [Sequential program]
    [Parallel program] :
  program α β → program α γ → program α (β × γ) :=
   λ αpβ αpγ => dup >=> αpβ |&| αpγ

infixl:60 " &|& " => productPar

def isZeroF: Nat → Bool := (. == 0)

def isOneF : Nat → Bool := (. == 1)

def oneF : Nat → Nat := λ _ => 1

def minusOneF : Nat → Nat := λ n => n - 1

def minusTwoF : Nat → Nat := λ n => n - 2

def addF : Nat × Nat → Nat :=
  λ ⟨n, m⟩ => n + m

def multiplyF : Nat × Nat → Nat := λ ⟨n, m⟩ => n * m

def isZero
    [Functional program] :
  program Nat Bool :=
    asProgram isZeroF

def isOne
    [Functional program] :
  program Nat Bool :=
    asProgram isOneF

def one
    [Functional program] :
  program Nat Nat :=
    asProgram oneF

def minusOne
    [Functional program] :
  program Nat Nat :=
    asProgram minusOneF

def minusTwo
    [Functional program] :
  program Nat Nat :=
    asProgram minusTwoF

def add
    [Functional program] :
  program (Nat × Nat) Nat :=
    asProgram addF

unsafe def parallelFibonacci
    [Functional program]
    [Sequential program]
    [Creational program]
    [Conditional program]
    [Parallel program] :
  program Nat Nat :=
    if_ isZero one $
      if_ isOne one $
        (minusOne >=> parallelFibonacci) &|&
        (minusTwo >=> parallelFibonacci) >=>
        add

structure FromComputationValuedFunction
    (computation : (Type → Type)) (α β : Type) where
  toComputationValuedFunction : α → computation β

instance [Applicative computation] :
    Functional
      (FromComputationValuedFunction computation) where
  asProgram :=
    λ αfβ => ⟨λ α => pure $ αfβ α⟩

instance [Functor computation] :
    Functorial
      (FromComputationValuedFunction computation) where
  andThenF :=
    λ ⟨αfcβ⟩ βfγ => ⟨λ α => βfγ <$> αfcβ α⟩

instance [Applicative computation] :
    Creational
      (FromComputationValuedFunction computation) where
  productSeq :=
    λ ⟨αfcβ⟩ ⟨αfcγ⟩ =>
      ⟨λ α => .mk <$> αfcβ α <*> αfcγ α⟩

instance [Monad computation] :
    Sequential
      (FromComputationValuedFunction computation) where
  andThenP :=
    λ ⟨αfcβ⟩ ⟨βfcγ⟩ =>
      ⟨λ α => αfcβ α >>= βfcγ⟩

def foldSum {γ β α : Type}
    (γfα : γ → α)
    (βfα : β → α)
    (sum : γ ⊕ β) : α :=
  match sum with
  | .inl tc => γfα tc
  | .inr tb => βfα tb

instance :
    Conditional
      (FromComputationValuedFunction computation) where
  sum :=
    λ ⟨γfγα⟩ ⟨βfγα⟩ =>
      ⟨foldSum γfγα βfγα⟩


class MonadAsync
    (computation : Type → Type) where
  async {α : Type} (ufα : Unit → α) : computation α

export MonadAsync (async)

instance
    [Monad computation]
    [MonadAsync computation] :
  Parallel (FromComputationValuedFunction computation) where
    bothPar := λ ⟨αfcγ⟩ ⟨βfcδ⟩ =>
      ⟨λ ⟨α, β⟩ =>
        async (λ (_: Unit) => αfcγ α) >>=
          λ cγ => async (λ (_: Unit) => βfcδ β) >>=
            λ cδ => .mk <$> cγ <*> cδ⟩

instance : Monad Task where
  pure := Task.pure
  bind := Task.bind

instance : MonadAsync Task where
  async := Task.spawn

abbrev TasksSpawningProgram :=
  FromComputationValuedFunction Task

def materializeTasksSpawning {α β : Type} :
  TasksSpawningProgram α β → (α → β) :=
    λ ⟨αftβ⟩ α => (αftβ α).get

unsafe def tasksSpawningFibonacci :=
  materializeTasksSpawning parallelFibonacci

-- #eval tasksSpawningFibonacci 10 -- also try 24 (takes longer)

[Luc Duponcheel]

Henrik, see attachment
WME.lean

[Henrik Böving]

First things first your definition is not unsafe if massaged sufficiently:

class Functional
    (program : Type → Type → Type) where
  asProgram {α β : Type} :
    (α → β) → program α β

export Functional (asProgram)

class Functorial
    (program : Type → Type → Type) where
  andThenF {α β γ : Type} :
    program α β → (β → γ) → program α γ

export Functorial (andThenF)

infixl:50 " >-> " => andThenF

class Sequential
    (program : Type → Type → Type) where
  andThenP {α β γ : Type} :
    program α β → program β γ → program α γ

export Sequential (andThenP)

infixl:50 " >=> " => andThenP

class Creational
    (program : Type → Type → Type) where
  productSeq {α β γ : Type} :
    program α β → program α γ → program α (β × γ)

export Creational (productSeq)

infixl:60 " &&& " => productSeq

class Conditional
    (program : Type → Type → Type) where
  sum {α β γ : Type} :
    program γ α → program β α → program (γ ⊕ β) α

export Conditional (sum)

infixl:55 " ||| " => sum

class Parallel (program : Type → Type → Type) where
  bothPar {α β γ δ : Type} :
  program α γ → program β δ → program (α × β) (γ × δ)

export Parallel (bothPar)

infixl:60 " |&| " => bothPar

def identity
    [Functional program] :
  program α α :=
    asProgram λ α => α

def let_
    [Functional program]
    [Sequential program]
    [Creational program] :
  program α β → program (α × β) γ → program α γ :=
    λ αpβ αaβpγ => identity &&& αpβ >=> αaβpγ

 def if_
    [Functional program]
    [Sequential program]
    [Creational program]
    [Conditional program] :
  program α Bool →
  program α β →
  program α β →
  program α β :=
    λ αpb t_apβ f_apβ =>
      let_ αpb $
        asProgram (
          λ αab => match αab with
            | ⟨α, true⟩ => .inl α
            | ⟨α, false⟩ => .inr α
        ) >=>
        t_apβ ||| f_apβ

def dup
    [Functional program] :
  program α (α × α) :=
    asProgram λ α => (α, α)

def productPar {α β γ : Type}
    [Functional program]
    [Sequential program]
    [Parallel program] :
  program α β → program α γ → program α (β × γ) :=
   λ αpβ αpγ => dup >=> αpβ |&| αpγ

infixl:60 " &|& " => productPar

def isZeroF: Nat → Bool := (. == 0)

def isOneF : Nat → Bool := (. == 1)

def oneF : Nat → Nat := λ _ => 1

def minusOneF : Nat → Nat := λ n => n - 1

def minusTwoF : Nat → Nat := λ n => n - 2

def addF : Nat × Nat → Nat :=
  λ ⟨n, m⟩ => n + m

def multiplyF : Nat × Nat → Nat := λ ⟨n, m⟩ => n * m

def isZero
    [Functional program] :
  program Nat Bool :=
    asProgram isZeroF

def isOne
    [Functional program] :
  program Nat Bool :=
    asProgram isOneF

def one
    [Functional program] :
  program Nat Nat :=
    asProgram oneF

def minusOne
    [Functional program] :
  program Nat Nat :=
    asProgram minusOneF

def minusTwo
    [Functional program] :
  program Nat Nat :=
    asProgram minusTwoF

def add
    [Functional program] :
  program (Nat × Nat) Nat :=
    asProgram addF

partial def parallelFibonacci
    [Functional program]
    [Sequential program]
    [Creational program]
    [Conditional program]
    [Parallel program] [Inhabited <| program Nat Nat]:
  program Nat Nat :=
    if_ isZero one $
      if_ isOne one $
        (minusOne >=> parallelFibonacci) &|&
        (minusTwo >=> parallelFibonacci) >=>
        add

structure FromComputationValuedFunction
    (computation : (Type → Type)) (α β : Type) where
  toComputationValuedFunction : α → computation β

instance [Inhabited (computation β)] : Inhabited (FromComputationValuedFunction computation α β) where
  default := { toComputationValuedFunction := fun _ => default }

instance [Applicative computation] :
    Functional
      (FromComputationValuedFunction computation) where
  asProgram :=
    λ αfβ => ⟨λ α => pure $ αfβ α⟩

instance [Functor computation] :
    Functorial
      (FromComputationValuedFunction computation) where
  andThenF :=
    λ ⟨αfcβ⟩ βfγ => ⟨λ α => βfγ <$> αfcβ α⟩

instance [Applicative computation] :
    Creational
      (FromComputationValuedFunction computation) where
  productSeq :=
    λ ⟨αfcβ⟩ ⟨αfcγ⟩ =>
      ⟨λ α => .mk <$> αfcβ α <*> αfcγ α⟩

instance [Monad computation] :
    Sequential
      (FromComputationValuedFunction computation) where
  andThenP :=
    λ ⟨αfcβ⟩ ⟨βfcγ⟩ =>
      ⟨λ α => αfcβ α >>= βfcγ⟩

def foldSum {γ β α : Type}
    (γfα : γ → α)
    (βfα : β → α)
    (sum : γ ⊕ β) : α :=
  match sum with
  | .inl tc => γfα tc
  | .inr tb => βfα tb

instance :
    Conditional
      (FromComputationValuedFunction computation) where
  sum :=
    λ ⟨γfγα⟩ ⟨βfγα⟩ =>
      ⟨foldSum γfγα βfγα⟩


class MonadAsync
    (computation : Type → Type) where
  async {α : Type} (ufα : Unit → α) : computation α

export MonadAsync (async)

instance
    [Monad computation]
    [MonadAsync computation] :
  Parallel (FromComputationValuedFunction computation) where
    bothPar := λ ⟨αfcγ⟩ ⟨βfcδ⟩ =>
      ⟨λ ⟨α, β⟩ =>
        async (λ (_: Unit) => αfcγ α) >>=
          λ cγ => async (λ (_: Unit) => βfcδ β) >>=
            λ cδ => .mk <$> cγ <*> cδ⟩

instance : Monad Task where
  pure := Task.pure
  bind := Task.bind

instance : MonadAsync Task where
  async := Task.spawn

abbrev TasksSpawningProgram :=
  FromComputationValuedFunction Task

def materializeTasksSpawning {α β : Type} :
  TasksSpawningProgram α β → (α → β) :=
    λ ⟨αftβ⟩ α => (αftβ α).get

def tasksSpawningFibonacci :=
  materializeTasksSpawning parallelFibonacci

[Henrik Böving]

Looking at the coredump of the crash it very much is a stack size issue.

[Henrik Böving]

With the version of your code without unsafe (for reference the diff is)

141c141
< unsafe def parallelFibonacci
---
> partial def parallelFibonacci
146c146
<     [Parallel program] :
---
>     [Parallel program] [Inhabited <| program Nat Nat]:
157a158,160
> instance [Inhabited (computation β)] : Inhabited (FromComputationValuedFunction computation α β) where
>   default := { toComputationValuedFunction := fun _ => default }
>
230,231c233
< unsafe def tasksSpawningFibonacci :=
---
> def tasksSpawningFibonacci :=

The issue is that your parallelFibonacci attempts to establish a closure containing itself so that just loops (non tail recursively) forever.

    def parallelFibonacci._at_.tasksSpawningFibonacci.spec_0 (x_1 : @& obj) : obj :=
      let x_2 : obj := isZero._at_.parallelFibonacci._at_.tasksSpawningFibonacci.spec_0.spec_0;
      let x_3 : obj := one._at_.parallelFibonacci._at_.tasksSpawningFibonacci.spec_0.spec_1;
      let x_4 : obj := isOne._at_.parallelFibonacci._at_.tasksSpawningFibonacci.spec_0.spec_2;
      let x_5 : obj := parallelFibonacci._at_.tasksSpawningFibonacci.spec_0 x_1; <- CALL HERE
      inc x_5;
      let x_6 : obj := pap parallelFibonacci._at_.tasksSpawningFibonacci.spec_0._lam_0 x_5;
      let x_7 : obj := pap parallelFibonacci._at_.tasksSpawningFibonacci.spec_0._lam_1 x_5;
      let x_8 : obj := add._at_.parallelFibonacci._at_.tasksSpawningFibonacci.spec_0.spec_7;
      let x_9 : obj := pap parallelFibonacci._at_.tasksSpawningFibonacci.spec_0._lam_2 x_6 x_7 x_8;
      inc x_3;
      let x_10 : obj := if_._at_.parallelFibonacci._at_.tasksSpawningFibonacci.spec_0.spec_8._redArg x_4 x_3 x_9;
      let x_11 : obj := if_._at_.parallelFibonacci._at_.tasksSpawningFibonacci.spec_0.spec_8._redArg x_2 x_3 x_10;
      ret x_11

The code produced also looks quite similar on v4.21.0 and I get a similar crash there as well, curiously I do indeed not get a crash when I use the unsafe version. I suspect the compiler was holding back on some optimizations in the unsafe case in 21 and for that reason didn't optimize this? Either way it seems to me like this is broken.

[Luc Duponcheel]

Henrik,

Thanks for your constructive comments.

parallelFibonacci is not a program, it is a program specification.

The whole goal of my PSBP project
(Program Specification Based Programming)
is to separate program specifications from programs.

A program is a materialization corresponding to instances of the classes in terms of whose members a program specification is written.

Compare this with the painting
"Ceci n'est pas une pipe" of René Magritte
(https://en.wikipedia.org/wiki/The_Treachery_of_Images).
The paining is not a pipe.

I understand that the type system of Lean cannot infer a type for parallelFibonacci. As I already +/- stated, I am
"living on the dangerous fast lane".
Anyway, Lean (v21) could evaluate tasksSpawningFibonacci 10
for the materialization of the Task based instances of the classes involved.

So what do you mean precisely with
"Either way it seems to me like this is broken"?

I mean, what is this in that sentence?

Do you mean that Lean (v21) should not be able to evaluate
tasksSpawningFibonacci 10, or do you mean that Lean (v22) should be able to evaluate tasksSpawningFibonacci 10?

[Luc Duponcheel]

I understand that imporant an goal of Lean is to be able to learn Lean what concepts like groups, rings, fields, categories etc. are all about and that Lean is this very demanding (but also very helpful) student that can review your proofs (but can also infer proofs for you). So my goal was to teach Lean what programs are all about. I understand that Lean cannot infer a type for a program specification, but that should, i.m.h.o. not prevent it from interpreting programs and/or generating executable code for programs. And, yes, badly written programs (not badly written program specifications) will, for example, end up looping forever.

[Henrik Böving]

parallelFibonacci is not a program, it is a program specification.

Yes it is a program, a program that allocates a lot of closures that eventually get evaluated when your task framework kicks in. Even if it might seem to you like you have some abstract notion of program specification going on this is not what the Lean compiler thinks about your program. If you want a specification and only that instead of this recursive closure allocator you would need to use an inductive for your program specification type.

I understand that the type system of Lean cannot infer a type for parallelFibonacci. As I already +/- stated, I am "living on the dangerous fast lane".

as I demonstrated in my snippet it is perfectly possible to write your Lean file without unsafe.

"Either way it seems to me like this is broken"?
I mean, what is this in that sentence?

parallelFibonacci could always be compiled to an infinite non tail recursion that blows the stack and I am surprised that it ever worked at all.

[Luc Duponcheel]

Henrik,

first of all, thx for all your replies

FYI:

I the past, I have written a (more elaborated)
"Program Specification Based Programming" library
in Scala and Haskell.

I switched to Lean because of it's theorem proving capabilities. With the idea of writing an, agreed, somewhat opinionated, programming course.

The code of the course being a programming course for Lean itself.

About:

"... you would need to use an inductive for your program specification type ...

Will using code like below, using a structure, then solve my problem?

BTW:

I did not manage, yet, to use an inductive, maybe you can help?

Code listing

structure Functional (program : Type → Type → Type) where
  asProgram {α β : Type} : (α → β) → program α β

structure FromComputationValuedFunction
    (computation : (Type → Type)) (α β : Type) where
  toComputationValuedFunction : α → computation β

instance [Applicative computation] :
  Functional (FromComputationValuedFunction computation) where
    asProgram := λ αfβ => ⟨λ α => pure $ αfβ α⟩

[Luc Duponcheel]

Hernik,

About:

... parallelFibonacci could always be compiled to an infinite
non tail recursion that blows the stack ...

• could : yes
• should : no

I mean, given the instance definitions that decrease the
arguments of the two spawned parallelFibonacci's, more
precisely n to n-1 and n-2, Lean could, maybe, be
clever enough to compile to code that does not blow the stack,
(apparently it did with v21) or, at least, offer a compiler option
to not do it.

BTW:

I have had no problems with the unsafe sequential fibonacci,
(both its Active and Reactive implementation). Only the
Task based implementation gave me problems.

[Henrik Böving]

I mean, given the instance definitions that decrease the
arguments of the two spawned parallelFibonacci's, more
precisely n to n-1 and n-2

This analysis is wrong. The Lean program parallelFibonacci simply calls itself infinitely deep non tail recursively. It doesn't matter what program it specifies, the semantics of Lean dictate that what you are doing is not okay. As I have explained above your program is also broken in both of the versions if it is written out properly without unsafe and instead using partial. As to why the compilation behavior of an unsafe definition changed between 4.21 and 4.22 I don't know but what it is doing now is not wrong.

Note that a trick like you are doing here might work out trivially in a lazy language like Haskell because the closures there would not be evaluated eagerly. This is very much not the case in Lean. If you check the definition of docs#Applicative in Lean you will observe that Lean explicitly introduces a Unit -> thunk in the second part of the sequence in order to avoid evaluating it if it doesn't actually end up being called. You could try to do something similar with your sequencing mechanism.

[Luc Duponcheel]

Hello, I found out in the source code that the difference has been introduced in the nightly build of 2026-06-21 in the file CoreM.lean at line 670, setting the new code generator as default code generator to true.

Anyway, I have no problems with my sequential fibonacci only with my Task based parallel fibonacci. So, maybe, it is related to Task code as well (.cpp code because most .lean code involved is extern).

I have raised an issue :
https://github.com/leanprover/lean4/issues/10372

hopefully it will be considered by the compiler guru's.

[Ruben Van de Velde]

Impressive crystal ball you've got there!