stdout and stderr behavior

Stream: general

[Matthew Ballard]

Is there a way to write to either stdout or stderr without resorting to #print or C++?

[Matthew Ballard]

More generally what are the semantics of writing to stdout and stderr in Lean 3? Some experimentation has yielded unexpected (to me) behavior.

[Alex J. Best]

What are you trying to accomplish? Printing during program execution, during a tactic, or something else?
You can write to stdout using docs#io.print_ln, e.g. io_test.lean:

import system.io

meta
def main : io unit :=
do
  io.run_tactic (tactic.trace "I go to stderr"),
  io.print_ln "I go to stdout"

then try

lean --run io_test.lean > program.stdout 2> program.stderr

[Matthew Ballard]

Thanks. That was the behavior I observed. The only way I managed to get to stderr was via tracing in a def/lemma. Is this the only way to get to stderr?

[Matthew Ballard]

Generally stderr is much less crowded so parsing it with something external is cleaner.

[Alex J. Best]

You can use docs#tactic.unsafe_run_io to call io methods from the tactic monad

[Alex J. Best]

so

meta
def main : tactic unit :=
do
  tactic.unsafe_run_io $ io.print_ln "I go to stdout"

would let you trace some special tactic output to stdout if that is helpful?

[Alex J. Best]

Or do you want the reverse?

[Julian Berman]

It looks like there are "regular" file-writing looking methods if that helps too. E.g.:

import system.io
meta
def main : io unit :=
do
  stderr ← io.stderr,
  io.fs.put_str_ln stderr "asdf"

[Julian Berman]

(or io.fs.write, or etc.)

[Matthew Ballard]

Thanks. These are both helpful.

This plus poking at filtering out constants should solve my use case.

[Matthew Ballard]

More broadly I don't understand why Lean writes to stdout vs stderr and would appreciate any philosophical insight

[Mario Carneiro]

It is pretty standard for a language to provide a println like function that writes to stdout by default

[Matthew Ballard]

I agree with that. But why does tracing something in a proof environment write to stderr

[Mario Carneiro]

all of lean's diagnostic messages go to stderr, I think

[Matthew Ballard]

I would have thought errors and warnings would get pushed to stderr

[Matthew Ballard]

Unless I don't know how to use a computer (of which there is a serious chance), that is not the case

[Mario Carneiro]

Actually scratch that, it looks like all of lean's diagnostics go to stdout

[Matthew Ballard]

Except for tracing in a proof

[Matthew Ballard]

As Alex pointed out or directly writing there as Julian did

[Mario Carneiro]

hm, you're right, the trace function prints to stderr even though it says

This function has a native implementation that displays the given string in the regular output stream.

[Mario Carneiro]

It makes some sense for it to write to stderr since it's not sequenced with regular writes

[Matthew Ballard]

Seems like Lean 4 follows the Lean 3 approach too

[Mario Carneiro]

trace_state and tactic.trace also write to stderr

[Mario Carneiro]

What is your application?

[Matthew Ballard]

Hmm I should take a look at trace_state

[Mario Carneiro]

it uses trace_fmt internally, same with tactic.trace

[Mario Carneiro]

Perhaps the commonality here is that all the stderr-writing functions are using the "pure" write functions, either trace or trace_fmt

[Matthew Ballard]

I am yak-shaving an autograder inside GitHub classroom. I already have a Lean 4 program that reads from naive #print axiom' coming out of Lean 3 checking a file

[Matthew Ballard]

I would gain amusement from internalizing everything in Lean 3 but not much else

[Julian Berman]

My brain is mush at this hour but can you say more about what you're trying to do in the autograder? You're doing stuff like making sure students aren't cheating by adding axioms or whatever?

[Mario Carneiro]

The easiest thing to do would be to put a marker before the print axioms:

import system.io
#eval io.print_ln "==================="
#print axioms classical.em

[Julian Berman]

If so the programmer in me says you'll have a better time if you ignore both stdout and stderr and write to a stream you fully own with whatever info you're trying to extract

[Matthew Ballard]

https://github.com/c0ppelius/lean-autograding

[Julian Berman]

ha, ok or do the hacky thing and do that I guess

[Mario Carneiro]

then just trim everything before the marker in the output

[Matthew Ballard]

I did the hacky thing

[Mario Carneiro]

Or alternatively, just require that the lean proof is silent

[Mario Carneiro]

mathlib does that

[Matthew Ballard]

theorem check_problem1 : ∀ (x : Type), x = x :=
begin
  check_solutions,
end

#print "Problem 1"
#print axioms check_problem1
#print "---"

[Mario Carneiro]

oh yeah, I forgot about #print string

[Matthew Ballard]

Julian Berman said:

If so the programmer in me says you'll have a better time if you ignore both stdout and stderr and write to a stream you fully own with whatever info you're trying to extract

Yes, I agree that this seems smarter

[Mario Carneiro]

@Julian Berman The problem is that you can't control where #print axioms writes since it's not a regular tactic

[Matthew Ballard]

Exactly

[Mario Carneiro]

You can write your own print axioms though

[Matthew Ballard]

But you can probably filter the environment for constants

[Mario Carneiro]

I have a code snippet for that lying around somewhere

[Matthew Ballard]

If you want to drop when you find it, I would appreciate it

[Matthew Ballard]

I also wrote something that filters the environment by directory to read from a student's assignment

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/intuitionistic.20logic/near/224372208

[Matthew Ballard]

So I imagine it is not far from there to filter by constant

[Matthew Ballard]

Thanks

[Jason Rute]

Do you know about lean --json? It makes the output into a json stream and makes it easier to work with the output programmatically.

[Matthew Ballard]

Eric Wieser said:

I'm not sure about the attribute, but those meta defs look worth PRing to me

I echo this sentiment

[Matthew Ballard]

I know about the existence of lean --json but not much more. I should take a look

[Matthew Ballard]

Is it easy to understand what the keys are for the json stream?

[Jason Rute]

I think it is self explanatory, but not documented, if that makes sense.

[Matthew Ballard]

I can dump some stuff and learn

[Henrik Böving]

Matthew Ballard said:

I would have thought errors and warnings would get pushed to stderr

There are pretty standard tools that do print their trace to stderr, for example strace does so because the main program might be busy printing to stdout while it's spying on it. I think you can make an argument that it makes sense for the "tracing" and the "regular stdout" stream to be different because then you can, pipe/grep/whatever exactly the stream you want right in your shell instead of having to somehow split them up again.

[Henrik Böving]

At least that's how I've always used this eh "feature" of strace.

[Matthew Ballard]

Ok. I think I have better mental model. If I assume Lean’s purpose is telling you when your proof is correct/incorrect then warnings/errors go to the usual placestdout. Less relevant output gets piped to stderrto avoid clutter.