mirror of
https://github.com/compiler-explorer/compiler-explorer.git
synced 2026-07-18 02:06:47 -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>
5 lines
86 B
Lean4
5 lines
86 B
Lean4
def add (x y : Nat) : Nat := x + y
|
|
|
|
def main : IO Unit := do
|
|
IO.println (add 1 2)
|