big arrays

Stream: new members

[Alok Singh]

I tried #eval Array.range 1000000 and it instantly crashed with many lines like

#9716 _private.Lean.ToExpr.0.Lean.List.toExprAux._at_._eval.spec_0

Is this just not gonna work?

[Eric Wieser]

It's the printing that is falling

[Eric Wieser]

It's trying to produce the information needed to hover over a million infoview terms

[Robin Arnez]

You can test #eval (Array.range 1000000).take 100 or #eval (Array.range 1000000).size

[Eric Wieser]

Or use IO.println

[Artur Lojewski]

Alok Singh said:

I tried #eval Array.range 1000000 and it instantly crashed with many lines like

#9716 _private.Lean.ToExpr.0.Lean.List.toExprAux._at_._eval.spec_0

Is this just not gonna work?

Hi Alok,

I tried to run your example. Your stack size is probably limited. What I did: Set my stack size limit (under Linux: ulimit -s unlimited) to unlimited - and then it worked ... printing a lot of output.

The error seems to be in:

l___private_Init_Data_Format_Basic_0__Std_Format_spaceUptoLine

which is the generated C/C++ source from:

https://github.com/leanprover/lean4/blob/49546687d9e809101991d6d1770afc5ef5d1d200/src/Init/Data/Format/Basic.lean#L161

[Robin Arnez]

Well the problem is in

private def List.toExprAux [ToExpr α] (nilFn : Expr) (consFn : Expr) : List α → Expr
  | []    => nilFn
  | a::as => mkApp2 consFn (toExpr a) (toExprAux nilFn consFn as)

which recurses the entire 1000000 length list without tail call. So as long as you don't a bunch of megabytes of stack space, this will just fail

[Eric Wieser]

And after that it will probably crash the VSCode UI

[Aaron Liu]

Robin Arnez said:

Well the problem is in

private def List.toExprAux [ToExpr α] (nilFn : Expr) (consFn : Expr) : List α → Expr
  | []    => nilFn
  | a::as => mkApp2 consFn (toExpr a) (toExprAux nilFn consFn as)

which recurses the entire 1000000 length list without tail call. So as long as you don't a bunch of megabytes of stack space, this will just fail

Can we make it tail recursive?

[Alok Singh]

I specifically did it to see what would happen figuring printing would be
the issue. TIL/}. Can we tail recurse it?

[Robin Arnez]

Aaron Liu schrieb:

Can we make it tail recursive?

Sure, then it will fail to pretty-print it though:

import Lean

open Lean
private def List.toExprAux [ToExpr α] (consFn : Expr) : List α → Expr → Expr
  | [],    e => e
  | a::as, e => toExprAux consFn as (mkApp2 consFn (toExpr a) e)

instance {α : Type u} [ToLevel.{u}] [ToExpr α] : ToExpr (List α) where
  toTypeExpr := mkApp (mkConst ``List [toLevel.{u}]) (toTypeExpr α)
  toExpr l :=
    let nilFn := mkApp (mkConst ``List.nil [toLevel.{u}]) (toTypeExpr α)
    let consFn := mkApp (mkConst ``List.cons [toLevel.{u}]) (toTypeExpr α)
    List.toExprAux consFn l.reverse nilFn

instance {α : Type u} [ToLevel.{u}] [ToExpr α] : ToExpr (Array α) where
  toTypeExpr := mkApp (mkConst ``Array [toLevel.{u}]) (toTypeExpr α)
  toExpr a := mkApp2 (mkConst ``List.toArray [toLevel.{u}]) (toTypeExpr α) (toExpr a.toList)

#eval Array.range 1000000