run meta program from command line

Stream: metaprogramming / tactics

[Christian Merten]

I am trying to run some analysis on a directory containing .lean files, which all have .olean files already. The information that I want to extract from each file is contained in an environment extension. What I currently have is this (minimized of course, in particular I dropped the logic for extracting and processing the env extension state):

import Lean
open Lean Elab

def countDecls (ns : Array Name) : IO Unit := do
  for name in ns do
    let _ ← importModules #[name] {}
    -- query some information from an environment extension
    IO.println s!"queried information: ..."

def pathToModule (path : IO.FS.DirEntry) : Name :=
  let fp := (path.path.toString.replace "/" ".").replace ".lean" ""
  fp.toName

def countAllInDir (path : System.FilePath) : IO Unit := do
  let ns := (← path.readDir).map pathToModule
  countDecls ns

#eval countAllInDir "directory"

The problem is that if the directory contains more than a few (say 5) files, my computer runs out of memory. Monitoring the memory usage with top shows that memory usage is monotonically increasing on each processed file. So clearly, I am doing something wrong here. Do I need to free some memory allocated by importModules? Or is there a cheaper way to extract environment extension data from an .olean file?
(I looked into Shake/Main.lean which uses docs#Lean.readModuleData, but I have no idea how to extract environment extension data from that).

[Kim Morrison]

docs#Lean.withImportModules

[Christian Merten]

Thanks, that worked, after figuring out I have to manually complicate expressions so that they can escape withImportModules (concretely, I had name : Lean.Name queried from the environment which I had to turn into name.toString.toName).