env using withImportModules

Stream: lean4

[Adam Topaz]

I came across something the following today:
Compare the following two pieces of code.

import Batteries.Lean.Util.Path
import Mathlib.Lean.CoreM

open Lean
def main : IO Unit := do
  searchPathRef.set compile_time_search_path%
  CoreM.withImportModules #[`Mathlib] do
    let env ← getEnv
    println! env.constants.toList.length

vs. the following:

import Batteries.Lean.Util.Path
import Mathlib.Lean.CoreM

open Lean
def main : IO Unit := do
  searchPathRef.set compile_time_search_path%
  let env ← CoreM.withImportModules #[`Mathlib] getEnv
  println! env.constants.toList.length

The first one works as expected, but the second gives a nonzero exit code and doesn't print anything. The thing is, in my mental model these two programs are equivalent, so I'm interested in understanding why they're behaving differently.

[Sebastian Ullrich]

This is a bug in Mathlib, that function must be unsafe. Please read docs#Lean.withImportModules.

[Eric Wieser]

Marking it unsafe wouldn't change anything here, right?

[Sebastian Ullrich]

It would hopefully make you think twice whether you've used unsafe correctly, which is not possible in the second code block

[Adam Topaz]

Thanks. What’s the preferred way to get an env in IO from an import while still allowing references to it?

[Eric Wieser]

I think you're expect to do all the work inside the withImportModules?

[Adam Topaz]

The thing is, I’m getting some unexpected stack overflow if I try to do my computation inside of the withImportModules so I explicitly want to try to do it in IO to diagnose the issue

[Henrik Böving]

You can run the binary in gdb until it stack overflows and take a look at the back trace for a first clue as to what is going wrong.

[Adam Topaz]

What is gdb?

[Henrik Böving]

Okay if you don't already know GDB my suggestion is probably not useful for you. If you still want to try: its a CLI based C debugger (the GNU debugger) that you can use to....well debug compiled lean projects. You would run gdb <binary> and then in the gdb shell run to execute the program and then when it crashes bt to get a backtrace.

[Adam Topaz]

Okay, I have it figured out now. Thanks all for the help! FWIW, the issue arose from the toJson instance for lists. Here is a minimized main function illustrating the issue:

def main : IO Unit := do
  println! toJson <| List.range 100000

[Kim Morrison]

@Adam Topaz, could you make an issue for that?

[Adam Topaz]

Will do. I'll do some more digging first (e.g. the same issue happens for Array, and the list instance uses that one)

[Eric Wieser]

I think the issue is the Json to string instance

[Adam Topaz]

Yeah I think you’re right

[Eric Wieser]

In fact, its the format to string one

[Eric Wieser]

run_cmd do
  let x := Lean.toJson <| List.range 100000
  pure (toString x).length

is fine

[Adam Topaz]

I'm not so sure... this still gives a stack overflow:

run_cmd do
  let x := Lean.toJson <| List.range 100000
  let e := (toString x).length
  println! e

[Adam Topaz]

I can't come up with an example that doesn't use Json, and only uses some large term of Format.