Zulip Chat Archive

Stream: lean4

Topic: Stack overflow when enumerating a matrix

Sofia (Nov 06 2021 at 08:45):

Hello world. Can you increase the stack size?

Stack overflow detected. Aborting.

Alternatively is there a better way to initialize an array/matrix over a function of its coordinates which does not lead to exhausting the stack?

List.range height
|> List.map (fun y => List.range width |> List.map (f . y))
|> List.join
|> List.map Nat.toUInt8
|> List.toArray
|> ByteArray.mk

Sofia (Nov 06 2021 at 08:46):

I'm trying to render images. 144p works, but any higher 16:9 resolution exceeds the limit.

Huỳnh Trần Khanh (Nov 06 2021 at 08:47):

run ulimit -s unlimited before running your program

Huỳnh Trần Khanh (Nov 06 2021 at 08:47):

that is if you're on linux

Sebastian Ullrich (Nov 06 2021 at 08:48):

Allocating a/multiple cons cells per pixel doesn't sound very efficient to begin with. You should create the array using ByteArray.mkEmpty <size> and then manipulate it using ByteArray.set!.

Sebastian Ullrich (Nov 06 2021 at 08:50):

It's not as nicely functional as your version, but should be vastly more efficient

Thanks for the suggestion. Either way I'll abstract around it because this really should just be its own function on the (Byte)Array types IMHO. Lean 3 has Steam.approx to construct lists from functions. Not quite sure how the Lean 4 streams work, but did note no approx function.

Sofia (Nov 06 2021 at 09:13):

Doesn't need to be super functional anyway. At least an excuse to use parallel for-in-do.

def bytearray_from_matrix (width height : Nat) (f : Nat -> Nat -> Nat) : ByteArray := do
    let mut res := ByteArray.mkEmpty (height * width)
    for x in List.range width, y in List.range height do
        res := res.set! (y * width + x) (f x y |> Nat.toUInt8)
    res

Sofia (Nov 06 2021 at 09:14):

Next question: is either Lean 4 or C smart enough to optimize away that multiplication. I sure hope so. But don't quite know the behavior of the parallel for loop here. Any insight?

Sofia (Nov 06 2021 at 09:15):

Specifically the order of its iteration.

Sofia (Nov 06 2021 at 09:18):

Can confirm it behaves better with the stack.

Sofia (Nov 06 2021 at 09:21):

Uhh... My array is empty. o.o

Sofia (Nov 06 2021 at 09:23):

Seems set fails. Pushing makes more sense anyway.

let mut res := ByteArray.mkEmpty (height * width)
for y in List.range height do
    for x in List.range width do
        res := res.push (f x y |> Nat.toUInt8)
res