mixing monads

Stream: general

[Patrick Massot]

Is there any way to mix the io and tactic monads? There lots of metaprogramming stuff with type tactic something and I would like to write the result to a file. I know I can use tactic.trace and redirect output to a file. But it would feel much cleaner to directly write to a file from Lean.

[Floris van Doorn]

Yes, there is docs#tactic.unsafe_run_io

[Jason Rute]

But as a note, I think if you are running Lean from the server (e.g. in vs code), you can’t use io inside a tactic to write to stdout, but I do think you can still write to a file which is what you want. If running lean from the command line, you can use io to write wherever you like.

[Jason Rute]

This might be a good place to mention (based on the title of the thread) that we now have ways to pass between the tactic, parser, and io monads:

• tactic inside io: docs#io.run_tactic (Starts up a tactic state with the same environment as io and a trivial |- true goal.)
• tactic inside parser : docs#lean.parser.of_tactic (So common that tactics are cast to parsers inside a parser monad.)
• io inside tactic: docs#tactic.unsafe_run_io (Is "unsafe" because one can use it to run stuff on command line, modify files, and send information over the internet. Also, it can make tactics nondeterministic.)
• parser inside tactic: docs#lean.parser.run and docs#lean.parser.run_with_input (The former runs a parser on an empty string to parse. The latter has you specify the string to parse.)

[Patrick Massot]

Thanks Floris and Jason.

[Ramon Fernandez Mir]

Hi, this should probably go in #lean4, but do you know what are counterparts of these are in Lean 4? In particular, how can one do something like tactic.unsafe_run_io. I know there is unsafeIO, but then the whole thing is marked as unsafe and cannot be used in proofs...

[Yakov Pechersky]

What would you want your IO tactic step to do?

[Ramon Fernandez Mir]

I'm reading an Array from a file and would like to plug it into a proof.

[Sebastian Ullrich]

TacticM is based on IO

[Ramon Fernandez Mir]

Wow, thanks, that is very neat! I'm amazed at how straightforward the solution to my problem is:

def test {α} (i : IO α) : TacticM α := do
  pure (← i)

[Sebastian Ullrich]

Or,

def test (i : IO α) : TacticM α := do
  i

:)