Testing commands help

Stream: lean4

[Josh Clune]

Hello,

I'm trying to figure out the best approach for testing a command that I've been working on. Specifically, I'm interested in measuring speed and viewing the outputs of the command on a large number of tests. The two main approaches I'm considering are compiling an executable that will run the command or writing a lake script that will run/test the command. But I've been having trouble figuring out how to get either approach to work.

For the first approach, I just can't seem to figure out how to invoke the command from IO. I know that for testing TacticM, TermElabM, MetaM, and CoreM functions, there are .run and .run' functions that let me do things like:

import Lean

open Lean
open Lean.Elab.Tactic

def metaMFunction : Lean.MetaM String := return "hi"

def main : List String → IO UInt32 := fun args => do
  let env : Lean.Environment ← Lean.mkEmptyEnvironment
  let fileName : String := sorry
  let fileMap : FileMap := sorry
  let (s, _) ← metaMFunction.run'.toIO {fileName, fileMap} {env}
  IO.println s
  return 0

Is there anything analogous for CommandElabM? Likewise, if I'm defining a command via a macro, is there anything analogous for MacroM?

For the second approach, I've had a bit more success writing a script in my lakefile:

import Lake

open Lake DSL

package Duper {
  precompileModules := true
}

lean_lib Duper

@[defaultTarget]
lean_exe defaultExe {
  root := `Main
}

open Std
open System

def runTest (lean : FilePath) (leanPath : SearchPath)
  (test : FilePath) : IO UInt32 := do
  IO.println s!"Start : {test}"
  let out ← IO.Process.output {
    cmd := lean.toString
    args := #[test.toString],
    env := #[("LEAN_PATH", leanPath.toString)]
  }
  -- I can run whatever tests I want to check that out.stderr and out.stdout are as I want
  return 0

/--
Run tests.
USAGE:
  lake script run test
Run tests.
-/
script test args do
  let lean ← getLean
  let leanPath ← getAugmentedLeanPath
  let task ← IO.asTask (runTest lean leanPath args[0]!)
  let code ← IO.ofExcept task.get
  return code

Although this mostly works in that lake script run test does basically what I want, I've found that with my current setup, the script test does not appear to be using precompiled modules. Since I'm interested in measuring speed (and since my command is sensitive to the heartbeat differences that arise when using or not using precompiled modules), this code doesn't quite do what I need it to. Is there some way to modify this code/approach to make sure that the precompiled modules are used?

Alternatively, if there's some other better way of testing commands, I would be totally open to that as well. Thanks!

[Arthur Paulino]

Sorry, what do you mean by "test commands"?
#xy: have you seen LSpec? https://github.com/yatima-inc/LSpec

[Josh Clune]

Ah, sorry I wasn't really clear. I'm working on a command that takes a filepath and proof as input, parses the corresponding file, builds a goal, tries to prove said goal with the input proof, and then uses Lean.logInfo to print some stuff.

If I write this command in some file ex.lean, then I can see the output either by viewing it in VSCode or by running lake env lean ex.lean. However, viewing output in VSCode doesn't let me easily run the command many times and see all the outputs/timings at once, and lake env lean ex.lean currently has the same issue my script file does that it will run the command without precompiled modules turned on.

So at the end of the day, when I say test my command I mean I want to be able to run my command a bunch of times on various inputs and see the resulting outputs, and I want to do this in such a way that when the command is run, it is run with precompiled modules.

I haven't seen LSpec before, and it seems interesting (thanks for the link), but I think the problem it's trying to solve is different from the problem I'm currently having.

Edit: Also, if possible, I'm trying to do this in such a way that I not only can see the outputs, but I can run various tests/checks on the outputs in Lean automatically (e.g. at the end of runTest in the lakefile I provided) rather than having to do that separately.