Lean produces no output if it exits early

[tydeu]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

If Lean exits (due to a crash or calling IO.Process.exit), Lean does not print any of the logged messages to the terminal. This makes it potentially very difficult to debug where a crash occurred and means any information prior to the crash is totally lost.

Steps to Reproduce

#eval IO.println "not shown"
#eval show IO PUnit from do
  IO.Process.exit 1

Expected behavior:

Lean to print not shown and then exit.

Actual behavior:

Lean exits without printing anything.

Reproduces how often:

Always.

Versions

Windows 10 20H2 Lean (version 4.0.0-nightly-2022-05-27, commit 3be437cad378, Release)

Additional Information

From looking at the code for Elab.runFrontend, this occurs due to the message log being printing only after every command is run. One potential solution would be print and empty the message log after each command rather than only at the end. This would still not print intra-command messages logged before a crash, but it would still be a major improvement.

Another solution is to introduce a saveMessages flag into CommandElabM that saves messages to the MessageLog if set, but otherwise just outputs them immediately. The manner in which this is done could be determined by an additional outputMessage : IO PUnit field to make it customizable (e.g., so that Lake, for instance, can output messages to stderr rather than stdout).