This avoids the temporary files workaround on macOS and Windows, and makes sure
we can process a `#eval` command and write messages to stdout at the same time.
Consider the following example
```lean
def div!: Nat → Nat → Nat
| x, 0 => panic! "division by zero"
| x, y => x/y
def weird (x : Nat) : MetaM Nat :=
unless (x > 0) (throwOther "x == 0") *>
let y := div! 10 x;
pure y
```
If we execute `weird 0`, it produces a "division by zero" panic
message.
This is a simple version of a much bigger function in the new
frontend.
This is not due to a bug in the compiler.
It produces the panic message because of the `do`-encoding
refactoring. Recall that, a few months ago,
we started to compile `do a; b` as `a *> b` (i.e., `seqRight a b`).
Thus, the example above is
`seqRight action1 (let y := div! 10 x; pure y)`
where `action1` is the `unless ...`.
In A-normal form, this is equivalent to
```lean
let y:= div! 10 x;
let action2 := pure y;
seqRight action1 action2
```
Thus, we execute `div! 10 x` before we even execute the `seqRight`.
This is counterintuitive and demonstrates once again how impure
features such as `panic!` are dangerous.
This commit reverts the `do`-encoding refactoring, and encodes
`do a; b` as `a >>= fun _ b` as we did in Lean3.
cc @Kha
Before this commit
```lean
pattern <- action
```
was being translated by the old frontend into
```lean
pattern <- action | matchFailed
```
This produced counterintuitive behavior, and performance problems when
tryin to synthesize `MonadFail` instances.
BTW, the new frontend does not implement this feature. I didn't even
remember the old frontend did this.
I will also remove the class `MonadFail` from stdlib.
cc @Kha @dselsam
@cipher1024 I modified your fix. It would produce memory leaks if the
code executed by #eval modifies the stdout.
Here is the problem.
- Your replaces the handler with some new handler `H` and stores the
old handler `O` in a `flet`.
- Code is executed and replaces the stdout handler with `H'`. The `H`s RC is
decremented and `H'`s RC is incremeneted. So far, so good.
- Now, the destructor of your `flet` is executed, and it replaces `H'`
with `O`, but `H'` RC is not decremented.
