mirror of
https://github.com/compiler-explorer/compiler-explorer.git
synced 2026-09-10 19:17:52 -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>
53 lines
2.0 KiB
TypeScript
53 lines
2.0 KiB
TypeScript
// Copyright (c) 2022, Compiler Explorer Authors
|
|
// All rights reserved.
|
|
//
|
|
// Redistribution and use in source and binary forms, with or without
|
|
// modification, are permitted provided that the following conditions are met:
|
|
//
|
|
// * Redistributions of source code must retain the above copyright notice,
|
|
// this list of conditions and the following disclaimer.
|
|
// * Redistributions in binary form must reproduce the above copyright
|
|
// notice, this list of conditions and the following disclaimer in the
|
|
// documentation and/or other materials provided with the distribution.
|
|
//
|
|
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
|
// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
|
// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
|
// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
|
|
// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
|
// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
|
// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
|
// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
|
// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
|
// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
|
// POSSIBILITY OF SUCH DAMAGE.
|
|
|
|
// note that these variables are saved to state, so don't change, only add to it
|
|
export enum DiffType {
|
|
ASM = 0,
|
|
CompilerStdOut = 1,
|
|
CompilerStdErr = 2,
|
|
ExecStdOut = 3,
|
|
ExecStdErr = 4,
|
|
GNAT_ExpandedCode = 5,
|
|
GNAT_Tree = 6,
|
|
DeviceView = 7,
|
|
AstOutput = 8,
|
|
IrOutput = 9,
|
|
RustMirOutput = 10,
|
|
RustMacroExpOutput = 11,
|
|
RustHirOutput = 12,
|
|
ClojureMacroExpOutput = 13,
|
|
YulOutput = 14,
|
|
LeanCOutput = 15,
|
|
}
|
|
|
|
export type DiffState = {
|
|
lhs: number | string;
|
|
rhs: number | string;
|
|
lhsdifftype: DiffType;
|
|
rhsdifftype: DiffType;
|
|
lhsextraoption?: string;
|
|
rhsextraoption?: string;
|
|
};
|