Fixes
https://github.com/compiler-explorer/compiler-explorer/issues/5634.
Adds the Lean 4 language and compiler.
> Lean is an open-source programming language and proof assistant that
enables correct, maintainable, and formally verified code
Since it was first requested in
https://github.com/compiler-explorer/compiler-explorer/issues/5634, it
has become increasingly relevant due to interest in AI-assisted theorem
proving, formalized mathematics, and verified software.
---
Lean compiles in two steps: first to C source code using the `lean`
executable, and then to assembly using the `leanc` compiler distributed
with Lean (I believe it's Clang).
The PR also includes a pane to visualize the emitted C source code that
was modelled after the panes for Rust and Haskell IRs and after the C
preprocessor pane for clang-format integration. Lean outputs mostly
unindented C code, so I enabled the formatter by default.
See companion infrastructure PR at
https://github.com/compiler-explorer/infra/pull/2130.
<img width="3024" height="1720" alt="image"
src="https://github.com/user-attachments/assets/5e7a1e91-e748-4599-8190-d3cb09fca503"
/>
---------
Co-authored-by: Matt Godbolt <matt@godbolt.org>