Write errors to STDERR

[pavelbraginskiy]

If I'm running Cryptol in batch mode, I want to be able to separate actual output from errors and messages such as Loading module Cryptol.

[brianhuffman]

Below is a list of some different kinds of output that Cryptol produces. Which of these, exactly, do you think should go to stderr vs stdout?

1. "Loading" messages for modules
2. Result values from evaluation
3. Run-time exceptions from evaluation (e.g. "division by 0")
4. Parse errors for Cryptol code
5. Type errors for Cryptol code
6. Counterexamples from :prove, :check, or :exhaust
7. Witnesses from :sat
8. "Unsatisfiable" message from :sat

Also, if you want to filter out the "Loading module" messages, we could consider adding an option like cryptol --quiet to suppress these.

[pavelbraginskiy]

I use Cryptol in batch mode as part of an automated script. I only want the results of evaluations, everything else I want to log in case something goes wrong for easier debugging.

Currently I have a setup where I do cryptol -b chk.cl | grep -v '^Loading module|^Assuming . =' | tee >(grep -i error && echo 'A cryptol error occured!' >>err.log) | # rest of pipeline. I'd instead like to simplify this to cryptol -b chk.cl 2>>err.log | # rest of pipeline and get more useful logging in the process.

So ideally for my use case, only 2. from that list would go to stdout. In addition, I think the messages saying Assuming a = ... and [warning] messages shold also go to stderr.

I personally don't use :sat anywhere, so I don't know what to think about 7. and 8..

[yav]

I would also add:

9. output of trace. In Haskell this goes to stderr

I would say that 6, 7, and 8 should probably go to stdout as they are the "propoer" result of the command.

[brianhuffman]

I had a go at implementing output to stderr. One big problem is that it breaks our testing framework: Because stdout and stderr are buffered differently by the OS, we lose guarantees about relative ordering of output. Stuff written to stderr shows up earlier in the output than it is supposed to, and I suspect that it's not even deterministic.

If the ultimate goal is simply to have the cryptol binary output only evaluation results, maybe this is better achieved by providing more control over verbosity via command-line options.

[pavelbraginskiy]

That would work, having the additional info for logs would be ideal though.

[atomb]

The use case described here could probably be better supported by the RPC API being developed here.