Step by step logging in main

Stream: new members

[Thomas Vigouroux]

Hey there,

I would like to have a main function that does:

def main: IO Unit := do
  IO.println "Before a"
  let a := fa args
  IO.println "After a"

When I do that in lean (assume we wait a few seconds in fa args), the text is all printed at once at the very end of the execution.

Do I have a way to "force" the execution to be step-by-step ?

[Henrik Böving]

That's not the case, if you run the binary that is generated from this code the IO will happen "step by step" and not at once in the end

[Thomas Vigouroux]

Oh I guess I was not clear.
My problem is that (looking at the binary), lean computes fa args during initialization of the binary, and then executes the body on the function.

I'd like to force fa args being computed in order, instead of at initialization

[Henrik Böving]

you can disable closed term extraction with set_option compiler.extract_closed false

[Thomas Vigouroux]

That worked, thank you very much !

[Thomas Vigouroux]

One last question while we're at it.
I have a monad to which I want to add an IO effect, is there an easy way to do so ?

[Thomas Vigouroux]

Basically I have a monad that I use to make a computation and I'd like to have a step where I print stuff to the screen in between computations

[Henrik Böving]

Do you know about monad transformers?

[Thomas Vigouroux]

Kind of, I'm reading the "Functionnal programming in Lean" about that ;-)

[Thomas Vigouroux]

But I can't find an IO transformer

[Henrik Böving]

That's what you want to use^^

[Henrik Böving]

Right

[Henrik Böving]

IO does not have a transformer, you would usually write your monad like ReaderT SomeContext <| StateT SomeState IO so IO would always be at the bottom of your monad stack.

[Eric Wieser]

If working over a general monad, you can use [MonadLiftT IO m], right?

[Thomas Vigouroux]

Actually let me add a little more context.
My goal is to prove of disprove that each turing machine in a set terminates.
My way into that is to have "deciders" which are algorithms which try to prove that the machine halts (or loops forever).

My idea was to have a monad like that, in order to chain deciders:

inductive HaltM (M: Machine) (α: Type u)
| unknown: α → HaltM M α
| halts_prf : M.halts → HaltM M α
| loops_prf : ¬M.halts → HaltM M α

Then if my decider has the type Unit -> HaltM M Unit I can chain them to have a bigger decider that tries them all, right ?

[Thomas Vigouroux]

Conveniently, stepping a machine can also give me an instance of this monad, that gives me either the next state in .unknown or the proof that the machine halts (we reached a halting state)

def Machine.step (M: Machine) (C: Config): HaltM M Config := ...

[Thomas Vigouroux]

Now let's say I want to extend my deciders to allow them to print stuff on the screen, what would their return type be ?

I can't see if it is IO (HaltM ...) or some kind of other thing

[Thomas Vigouroux]

In particular, I have a decider that looks somewhat like this:

def looperDec (M: Machine) (init: Config) : IO (HaltM M Unit) := do
      let state1: Config := (M.step init >>= M.step)
      let state2: Config := M.step init
      ...

But I get the following error:

type mismatch
  M.step init >>= M.step
has type
  HaltM M Config : Type
but is expected to have type
  Config : Type