Stack overflow with Array.mk

Stream: lean4

[Ioannis Konstantoulas]

Hello all;

I am testing Lean's capacity for memory allocation, and ran into the following problem (mwe follows):

def OnesList : List Nat := List.replicate (1000*1000*100) 1
def OnesArr := Array.mk OnesList
def One := OnesArr[1]?

-- main file
def main : IO Unit :=
  IO.println s!"Hello, {One}!"

Compiling this with lake build and running produces:

> lake build && time ( ./build/bin/performance )
[0/4] Building Performance
[1/4] Compiling Performance
[1/4] Building Main
[2/4] Compiling Main
[4/4] Linking performance

Stack overflow detected. Aborting.
[2]    168414 IOT instruction (core dumped)  ( ./build/bin/performance; )
( ./build/bin/performance; )  2.23s user 12.17s system 56% cpu 25.583 total

I expected an overflow for the List type, but not when making the array; constructing the list and accessing some elements directly is fine:

lake build && time ( ./build/bin/performance )
[0/4] Building Performance
[1/4] Compiling Performance
[1/4] Building Main
[4/4] Linking performance
Hello, world!
Hello, (some 1)!
( ./build/bin/performance; )  2.50s user 4.78s system 95% cpu 7.627 total

So I have a couple of questions:

1. Why does making the array from the list cause an overflow? Is this expected?

2. If we want to allocate and initiate large arrays, and producing them from lists overflows, what is the standard way to do it? Do we need to push or repeatedly self-append manually, or is there an optimized function?

Thanks for your time!

[Ioannis Konstantoulas]

Addendum: my lean version is Lean (version 4.0.0-nightly-2023-07-22, commit 544b704a2589, Release).

[Daniil Kisel]

For this specific case there is Array.mkArray, which is equivalent to mk + List.replicate but is implemented in C.

[Scott Morrison]

Also, your examples aren't that helpful, as you haven't shown us the code for both runs.

[Scott Morrison]

If you're trying to do large scale things, it seems strange to start with List, rather than just directly working with Array.

[Ioannis Konstantoulas]

Right, but since there does not seem to be any documentation for Array pointing to the right constructors vs wrong constructors, I am just experimenting and asking here. Is there a better workflow? Also, I am not sure what you mean, the code is right there, there is no other code.

[Ioannis Konstantoulas]

Oh, I see, I forgot to paste the non-array part.

[Ioannis Konstantoulas]

Here is the code for the second compilation.

def OnesList : List Nat := List.replicate (1000*1000*100) 1
def One := OnesList[1]?

-- main file
def main : IO Unit :=
  IO.println s!"Hello, {One}!"

[Ioannis Konstantoulas]

Daniil Kisel said:

For this specific case there is Array.mkArray, which is equivalent to mk + List.replicate but is implemented in C.

Thank you! Is there a corresponding function for List.iota which creates an array of consecutive integers?

[Daniil Kisel]

Not that I know of.

[Arthur Adjedj]

Ioannis Konstantoulas said:

Daniil Kisel said:

For this specific case there is Array.mkArray, which is equivalent to mk + List.replicate but is implemented in C.

Thank you! Is there a corresponding function for List.iota which creates an array of consecutive integers?

There isn't, but you can construct one yourself. Since the array will be modified in-place, you should still get pretty good performance out of it:

def IotaArr (size : Nat) := Id.run do
  let mut arr := Array.mkEmpty size
  for i in [0:size] do
    arr := arr.push i
  arr

def main : IO Unit :=
  let arr := IotaArr 10000000
  IO.println s!"Hello, {arr[10000]!}!"

[Sebastian Ullrich]

No need to pre-initialize the array, you can use mkEmpty with a given capacity + push

[Arthur Adjedj]

Fixed :thumbs_up: