Performance of Lists

Stream: lean4

[Yves Jäckle]

Hey!
In get a stack overflow for ( including on the web editor).

set_option maxRecDepth 9000000 in
#eval (List.range 175561).map (· +1)

I'm new to programming in general.
Is this because the code generated for lists is inefficient ? (though Array yields the same problem).
Is there a general way I allow lean to handle large computations without changing the implementation ?
Is my laptop just bad ?

[Julian Berman]

I'm not fully sure but it certainly seems like part of the answer is you're asking to print that giant thing. Are you really trying to do that, or just do some continued computation?

[Julian Berman]

E.g., with Array, this is fine:

def f := Array.range 175561
def g := f.map (· + 1)

#check g

#eval g[37]!

[Eric Wieser]

Julian Berman said:

I'm not fully sure but it certainly seems like part of the answer is you're asking to print that giant thing.

Worse, pretty-print as a Format object

[Eric Wieser]

This works fine:

set_option maxRecDepth 9000000 in
#eval toString <| (List.range 175561).map (· +1)

[Kim Morrison]

And even in this case you are benchmarking toString presumably! Throw in a Nat.sum before worrying about long lists.

[Julian Berman]

Unrelated but because I noticed it, does set_option maxRecDepth 0 PANIC for either/any of you?

[Julian Berman]

It does here (in nvim and VSCode, on 4.10.0-rc2) but seems not to in the web editor.

[Eric Wieser]

0 means "no stack!! only execute", as opposed to "as much stack as you like"

[Julian Berman]

Right I understand it's not what I wanted anyhow, but the PANIC was presumably unexpected

[Yves Jäckle]

Amazing, thanks :+1:

[Notification Bot]

Yves Jäckle has marked this topic as resolved.

[Gareth Ma]

Hi, this topic is quite interesting and I want to learn more about it. I looked at the implementation of Repr which I assume is where the Format comes from. Here are the relevant parts:

def Format.joinSep {α : Type*} [ToFormat α] : List α → Format → Format
  | [],    _   => nil
  | [a],   _   => format a
  | a::as, sep => as.foldl (· ++ sep ++ format ·) (format a)

protected def List.repr {α : Type*} [Repr α] (a : List α) : Format :=
  let _ : ToFormat α := ⟨repr⟩
  match a with
  | [] => "[]"
  | as => Format.bracket "[" (Format.joinSep as ("," ++ Format.line)) "]"

From what I can tell, List.repr is not recursive (as in recurse to itself) and just calls Format.joinSep, and neither is Format.joinSep which calls List.foldl. So the stack overflow occurs at List.foldl. But... List.sum also calls List.foldl??

[Notification Bot]

Gareth Ma has marked this topic as unresolved.

[Gareth Ma]

And this doesn't stack overflow

import Mathlib.Tactic
open Std Format
def add_up : List Nat → Nat
  | [] => 0
  | a::as => as.foldl (· + ·) a

def add_up_list (a : List Nat) : Format :=
  match a with
  | [] => "[]"
  | as => Format.bracket "[" (toString <| add_up as) "]"

set_option linter.setOption false
set_option trace.profiler true

#eval add_up_list (List.range 50000)

So does this mean String is the place overflowing? Or am I missing something stupid

[Mario Carneiro]

you are secretly calling Format.pretty there because you are passing a Format to #eval to show it. Format.pretty is bad at deep recursion if you hand it a deeply nested Format object

[Gareth Ma]

Ohh I see now, thanks! I think I also mixed up Format with String (due to the ++), so I didn't realise it's a nested tree instead of a string