Print from Rust

Stream: lean4

[Marcus Rossel]

If I run the following Rust function from Lean, it prints "Hello" to stdout:

fn printhello() {
  println!("Hello");
}

But if the function never returns, it never prints "Hello" as in the following:

fn nohello() {
  println!("Hello");
  loop {};
}

Is there a way to get nohello to print to stdout anyway?

---

#xy: I'm trying to print-debug from Rust. I think I have a non-terminating loop somewhere, and am trying to figure out where.

[Alex J. Best]

Do you need to flush stdout maybe on the rust side. Seems strange that it wouldn't print at all, more likely that it's just buffered

[Marcus Rossel]

@Alex J. Best I tried using io::stdout().flush(), but that didn't help.

[Julian Berman]

(I thought maybe so too, but Rust appears to still use line-buffering always according to https://github.com/rust-lang/rust/issues/60673 )

[Julian Berman]

If you strace do you see the syscall happen maybe?

[Eric Wieser]

How are you calling rust from Lean?

[Marcus Rossel]

Eric Wieser said:

How are you calling rust from Lean?

I should have mentioned that! It's as part of a tactic - so at compile time in MetaM.

[Eric Wieser]

So it's linked via extern, not run via a subprocess?

[Marcus Rossel]

Eric Wieser said:

So it's linked via extern, not run via a subprocess?

Exactly! (I'm setting up an mwe repo as we speak)

[Mauricio Collares]

(regarding the #xy-question, perhaps it would be useful to gdb attach to your process)

[Marcus Rossel]

Ok, here's a #mwe repo: https://github.com/marcusrossel/mwe/tree/main
But for some reason, right now it's not even printing "hello"/looping for the following:

import Lean
open Lean Meta Elab Tactic

@[extern "lean_printhello"]
opaque printhello : Unit → Unit

@[extern "lean_nohello"]
opaque nohello : Unit → Unit

def Unit.toExpr (_ : Unit) : MetaM Expr :=
  Lean.Meta.mkAppM ``Unit.unit #[]

elab "hello" : tactic => do
  let u := printhello ()
  (← getMainGoal).assign (← u.toExpr)

example : Unit := by
  hello

elab "nohello" : tactic => do
  let u := nohello ()
  (← getMainGoal).assign (← u.toExpr)

example : Unit := by
  nohello

(I added the Unit.toExpr dance in the hope that it would mean that Lean doesn't optimize away the calls to printhello and nohello - though I have no clue if that's necessary or effective.)

[Tomas Skrivan]

Does it work as expected if printhello and nohello live in IO monad?

[Tomas Skrivan]

I don't think that u.toExpr is preventing Lean from optimizing the calls away.

[Kyle Miller]

If it's not in the IO monad, I think the reliability of printing is more like dbg_trace, which will happen if it's forced to, but it might be eliminated. For example, I don't see any messages in

def printHello : Unit → Unit := fun _ => dbg_trace "hello"; ()

#eval printHello ()

[Leni Aniva]

Does it work if you print to stderr instead to remove the buffering?

[Marcus Rossel]

Leni Aniva said:

Does it work if you print to stderr instead to remove the buffering?

Using eprintln! didn't work either.

[Marcus Rossel]

Kyle Miller said:

If it's not in the IO monad, I think the reliability of printing is more like dbg_trace

I tried wrapping my function's return type in IO and using lean_io_result_mk_ok when returning the result from C. Should that be enough to see println!s? Because when the Rust function is non-terminating I still don't see the result of the println!.