Zulip Chat Archive

Stream: general

Topic: mixing monads

Patrick Massot (May 29 2021 at 15:33):

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 (May 29 2021 at 15:44):

Yes, there is docs#tactic.unsafe_run_io

Jason Rute (May 29 2021 at 15:52):

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 (May 29 2021 at 16:28):

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 (May 29 2021 at 16:31):

Thanks Floris and Jason.

Ramon Fernandez Mir (Jul 20 2021 at 17:41):

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 (Jul 20 2021 at 17:42):

What would you want your IO tactic step to do?

Ramon Fernandez Mir (Jul 20 2021 at 17:45):

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

Sebastian Ullrich (Jul 20 2021 at 18:25):

TacticM is based on IO

Ramon Fernandez Mir (Jul 21 2021 at 10:29):

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 (Jul 21 2021 at 11:22):


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


Last updated: Aug 03 2023 at 10:10 UTC