ImportGraph test memory errors:

Stream: new members

[Riyaz Ahuja]

Hello, I'm trying to get the ImportGraph of user-provided list of modules for a project of mine, but am recieving no output, and the terminal says that I'm erroring, but I am not seeing any standard error logs that I'm used to. Here is the MWE:

import Cli.Basic
import ImportGraph.Imports
import Mathlib.Lean.CoreM


open Lean Cli Environment

set_option autoImplicit true



def test (mods : List Name) (test_mod : Name) : IO UInt32 := do
  searchPathRef.set compile_time_search_path%

  let graph ← CoreM.withImportModules mods.toArray do
    let env ← getEnv
    return importGraph env

  let graph_output := graph.find? test_mod
  IO.println s!">> Graph: \n{graph_output}"
  return 0



def testImportCLI (args : Cli.Parsed) : IO UInt32 := do

  let modules_raw := args.positionalArg! "modules" |>.as! String
  let modules : List String := if modules_raw.isEmpty then [] else modules_raw.splitOn ","
  let mods := modules.map (fun m => m.toName)

  test mods mods[0]!


def test_import : Cmd := `[Cli|
  test_import VIA testImportCLI; ["0.0.1"]
"Test import graph."

  ARGS:
    modules : String; "List of modules to include in the prompts, separated by \",\"."
]

def main (args : List String) : IO UInt32 :=
  test_import.validate args

And my lakefile says:

import Lake
open Lake DSL

package «lean-training-data» {
  -- add any package configuration options here
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.17.0"

lean_lib Data where

@[default_target]
lean_exe build_rag where
  root := `Data.test_import
  supportInterpreter := true

If i run this script by the command line, I get:
image.png

And similarly, if i run the script by #eval, i get a message saying "Server process for file:///[MY MWE's PATH] crashed, likely due to a stack overflow or a bug.".

With some googling, it seems that exit code 139 represents a memory issue, which checks out with the #eval output. How do I go about fixing this?

[Riyaz Ahuja]

Ok, weird, it seems that if the CoreM code doesn't return anything, then it "works":

def test (mods : List Name) (test_mod : Name) : IO UInt32 := do
  initSearchPath (← getLibDir (← findSysroot))

  let _ ← CoreM.withImportModules mods.toArray do
    let env ← getEnv
    let g := importGraph env

    let graph_output := g.find? test_mod
    IO.println s!">> Graph: \n{graph_output}"

  return 0

Strange...

[Riyaz Ahuja]

For my purposes, this is a suitable workaround, but I am still a bit surprised by this behavior. I was able to reproduce it on 4.22 but still am a bit curious as to why the errors are happening in the first place.

[Henrik Böving]

withImportModules from mathlib is quite a footgun for this reason, the explanation can be found in the underlying function Lean.withImportModules which is marked as unsafe and has a doc string to explain this:

Creates environment object from imports and frees compacted regions after calling act. No live references to the environment object or imported objects may exist after act finishes. As this cannot be ruled out after loading environment extensions, importModules's loadExts is always unset using this function.

By returning a list of Name that reference Name objects from the imported modules you are breaking this invariant and causing a segfault.

[Riyaz Ahuja]

That makes sense, thanks.