Excessive Time and Memory Consumption of `ProcessCommads`

Stream: metaprogramming / tactics

[Kaiyu Yang]

Hi,

I'm using the following metaprogramming code to process files in mathlib. It works smoothly for most files. But for Mathlib/Data/Real/Basic.lean, it often takes more than 10 minutes and >64GB of memory. The most time-consuming part is IO.processCommands inputCtx parserState commandState. Note that checking Mathlib/Data/Real/Basic.lean directly only takes a few seconds and ~300MB of memory.

Anyone has ideas? Thanks!

import Lean

open Lean Elab System

unsafe def main (args : List String) : IO Unit := do
  let path := FilePath.mk "Mathlib/Data/Real/Basic.lean"
  let input ← IO.FS.readFile path
  let opts := Options.empty.setBool `trace.Elab.info true
  enableInitializersExecution
  let inputCtx := Parser.mkInputContext input path.toString

  println! "Parsing header..."
  let (header, parserState, messages) ← Parser.parseHeader inputCtx
  println! "Processing header..."
  let (env, messages) ← processHeader header opts messages inputCtx
  assert! ¬messages.hasErrors

  let env := env.setMainModule (← moduleNameOfFileName path none)
  let commandState := { Command.mkState env messages opts with infoState.enabled := true }
  println! "Processing commands..."
  let _ ← IO.processCommands inputCtx parserState commandState
  println! "Done!"

Steps to reproduce the problem:

1. Clone a new copy of mathlib4.
2. Create a new file named ProcessReal.lean with the content above.
3. Build mathlib: lake build
4. lake env lean --run ProcessReal.lean

[Adam Topaz]

I think it's because you're setting the option to be true, where you can just turn on infotrees in the info state and get the infotrees that way

[Adam Topaz]

It looks like you're already doing that on line -4, so just get rid of the let opts := ... line and it shold be fine

[Adam Topaz]

import Mathlib.Util.Time
import Lean

open Lean Elab System

unsafe def main : IO Unit := do
  let path := FilePath.mk ".lake/packages/mathlib/Mathlib/Data/Real/Basic.lean"
  let input ← IO.FS.readFile path
  enableInitializersExecution
  let inputCtx := Parser.mkInputContext input path.toString

  println! "Parsing header..."
  let (header, parserState, messages) ← Parser.parseHeader inputCtx
  println! "Processing header..."
  let (env, messages) ← processHeader header {} messages inputCtx
  assert! ¬messages.hasErrors

  let env := env.setMainModule (← moduleNameOfFileName path none)
  let commandState := { Command.mkState env messages {} with infoState.enabled := true }
  println! "Processing commands..."
  let state ← IO.processCommands inputCtx parserState commandState
  IO.println state.commandState.infoState.trees.size

#time #eval main

results in

time: 7921ms
Test123.lean:24:6
Parsing header...
Processing header...
Processing commands...
198

[Adam Topaz]

so now it takes about 8 seconds to elaborate the file, and you get all 198 info trees

[Adam Topaz]

(Note that I changed the filepath)

[Kaiyu Yang]

@Adam Topaz This works great! Thanks!