Mac Malone

To add on to this, `if-else` with `return` does compile the tail call correctly: ```lean partial def foobar (n : Nat) : Nat := do if n == 10 then...

> Keep in mind that `return` in do-notation is an _early exit_, My apologies, but I am not sure what you are getting at here. I am aware that `return`...

> But to really solve the TCO issue in general, including all the do sugar (the usual definition of "tail position" would not exclude these examples), what is needed is...

OOPS! I just realized I made a major error in my previous `foobar` and `pure_bar` definitions. They are both using `bar` rather than recursing on themselves. With the proper definitions...

> Right, these are orthogonal issues. `do` notation produces suboptimal desugaring involving lambdas when they aren't necessary, and mutual TCO doesn't work. I still find it interesting that you are...

@Vtec234 I think creating a new pipe would be a great idea! Then normal stdout output could just appear in the console (i.e., the VS Code 'Output' panel) like stderr...

@Kha > > This is due to Lake setting `LEAN_CC` to the compiler it discovers > > But why would it do that? `LEAN_CC` is intended to be "the C...

@Kha > > This feels rather unprincipled to me, but I guess I can make it work as stop-gap solution. > > It feels more principled to me than worrying...

@gebner > The bundled compiler doesn't work on nixpkgs, so there needs to be a way to override the override the bundled compiler and the override needs to be integrated...

@Kha > Hmm, seems to work fine in CI though? Yes, this is true, which is why I personally never reported these errors. For me, the following tests consistently break...