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).

[Christian Merten]

I am running into this again. What is the correct way to extract information from a withImportModules invocation? For simple things, such as name : Lean.Name the stupid name.toString.toName works, but for more complicated things I don't know how to trick Lean into creating a new memory reference.

A mwe:

import Lean
open Lean

unsafe def main : IO Unit := do
  _ ← initSearchPath ""
  let nm1 ← Lean.withImportModules #[`Lean] {} fun env => do
    return (env.constants.map₁.fold (init := #[]) fun r k _ => r.push k)[42]!.toString.toName
  IO.println s!"first name: {nm1}"
  let nm2 ← Lean.withImportModules #[`Lean] {} fun env => do
    return (env.constants.map₁.fold (init := #[]) fun r k _ => r.push k)[37]!
  IO.println s!"second name: {nm2}"

with corresponding section in lakefile.toml:

[[lean_exe]]
name = "bar"
root = "Bar"
supportInterpreter = true

yields on lake exe bar the output:

first name: Lean.Elab.Tactic.NormCast.evalConvNormCast._cstage2

and then aborts silently.

[Jannis Limperg]

Does it help if you do all your processing and printing inside the withImportModules? Also, note the new restriction about env extensions mentioned in docs#Lean.withImportModules; this may or may not cause problems for you.

[Christian Merten]

This would be equivalent to

    let env ← importModules #[name] {}
    /- processing goes here -/

right? In this case, I can't do that, because the memory needs to be freed, otherwise my memory runs out if processing, say, more than 5 files.