deep recursion in list.mmap

Stream: general

[Eric Wieser]

How am I supposed to write a for loop without hitting a deep recursion issue?

meta def main : io unit :=
do
  (list.iota 10000).mmap $ λ i, do
  { io.put_str (format!"{i}\n").to_string },
  pure ()
#eval main

gives

deep recursion was detected at 'formatter' (potential solution: increase stack space in your system)

[Eric Wieser]

This comment in doc-gen ran into the same issue:

Using environment.mfold is much cleaner. Unfortunately this led to a segfault, I think because
of a stack overflow. Converting the environment to a list of declarations and folding over that led
to "deep recursion detected". Instead, we split that list into 8 smaller lists and process them
one by one. More investigation is needed.

[Eric Wieser]

This seems to help:

/-- A version of `list.map` for `io` that does not consume the whole stack -/
def list.mmap_io {α β : Type*} (f : α → io β) (l : list α) : io (list β) :=
do
  (_, bs) ← io.iterate (l, ([] : list β)) (λ state, do {
    (a :: as, bs) ← pure state | return none,
    b ← f a,
    return (some (as, b :: bs))
  }),
  pure bs

Unfortunately I'm not allowed to @[vm_override] that

[Reid Barton]

docs#list.mmap' works

[Eric Wieser]

Not for n = 100000 it doesn't

[Reid Barton]

I would not try to process that big a list then

[Patrick Massot]

Yes, this is a very well-known issue in Lean 3. I also hit it badly with LeanCrawler.

[Eric Wieser]

Is there a github issue or prior zulip thread that comes to mind?

[Eric Wieser]

Reid Barton said:

I would not try to process that big a list then

such long lists originate from docs#environment.get_decls

(the application here was exporting symbol information from a git repo to use as links in LaTeX)

[Patrick Massot]

Eric, there is probably related info in the thread https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/random.20io.20output

[Mario Carneiro]

Eric Wieser said:

Reid Barton said:

I would not try to process that big a list then

such long lists originate from docs#environment.get_decls

You should not use get_decls if this is an issue. Instead use environment.fold and just do what you need to do on each decl as it goes by without buffering them all into a list

[Eric Wieser]

Doesn't that hit the same problem if I fold over a monad? (I haven't tried)

[Mario Carneiro]

No; for example you can call trace on all decls and nothing overflows. Building a list is also something you can do (this is how get_decls works after all), it's just consuming the large list that causes a stack overflow

[Eric Wieser]

Wild, thanks for the tip

[Eric Wieser]

The list.mmap_io definition above did also solve the problem though

[Eric Wieser]

But I guess only in one monad