mirror of
https://github.com/compiler-explorer/compiler-explorer.git
synced 2026-07-16 17:26:58 -04:00
a6cdc6a66d
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>