Memory increase in loops.

Stream: lean4

[Joseph Tooby-Smith]

On running the following mwe:

import Batteries.Lean.HashSet
import Lean

open Lean Elab System


unsafe def processFileHeader (file : FilePath) : IO Unit := do
  searchPathRef.set compile_time_search_path%
  let fileContent ← IO.FS.readFile file
  enableInitializersExecution
  let inputCtx := Parser.mkInputContext fileContent file.toString
  let (header, parserState, messages) ← Parser.parseHeader inputCtx
  let (env, messages) ← processHeader header {} messages inputCtx
  -- Other code to go here.
  pure ()

unsafe def main : IO Unit := do
  let file := ".lake/packages/mathlib/Mathlib/Algebra/AddConstMap/Basic.lean"
  for n in List.range 100 do
    println! "{n}"
    processFileHeader file

each step in the for loop in main leads to an increase in memory. It seems like the variables env and messages etc are held onto once the function processFileHeader is complete for each iteration. Is this the case? Is there a way to clear these variables to ensure they are not kept between iterations and memory doesn't explode.

(The code in processFileHeader is based on code from here)

[Joseph Tooby-Smith]

The memory still explodes with the more functional approach where main above is replaced with:

unsafe def main : IO Unit := do
  let file := ".lake/packages/mathlib/Mathlib/Algebra/AddConstMap/Basic.lean"
  (List.range 100).forM (fun _ => processFileHeader file)

[Henrik Böving]

env does not get free-d because it contains mmap-ed data. So in order to free env you need to free all of env at once. However that requires that not a single reference into env exists anymore which is an invariant that you have to ensure. There is unsafe functions like docs#Lean.withImportModules that do free the environment they create and are safe to call under the assumption that no references to objects in env exist anymore. You can imitate what they are doing under the hood to free and env if you want.

[Joseph Tooby-Smith]

Thanks @Henrik Böving ! Until I understand exactly how to do this, I'm going to follow the same workaround as  here, which is to use IO.Process.run to call another file containing processFileHeader .