printing the prover state after every tactic

Stream: lean4

[Sid]

Hi,

Is it possible to print the prover state after every tactic? I tried setting

set_option trace.compiler.ir.init true
set_option pp.all true

and running with

lean filename.lean

but that doesn't work and it doesn't print anything.

[Yury G. Kudryashov]

Why do you want this? If you want to talk to Lean from another program, then have a look at https://github.com/leanprover-community/REPL

[Sid]

Yury G. Kudryashov said:

Why do you want this? If you want to talk to Lean from another program, then have a look at https://github.com/leanprover-community/REPL

For some data generation but actually I realized that LeanDojo outputs goal information which might work.