mirrors/compiler-explorer
2
0
Fork 0
mirror of https://github.com/compiler-explorer/compiler-explorer.git synced 2026-07-16 17:26:58 -04:00
Code Issues Packages Projects Releases Wiki Activity

Add Lean (#8737)

Browse Source 
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>
This commit is contained in:
Francisco Giordano
2026-06-02 14:19:29 -03:00
committed by GitHub
parent cc515ed658
commit a6cdc6a66d
27 changed files with 937 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
.github/labeler.yml vendored
View File

@@ -246,6 +246,13 @@
- 'lib/compilers/kotlin.ts'
- 'etc/config/kotlin.*.properties'
'lang-lean':
- changed-files:
- any-glob-to-any-file:
- 'lib/compilers/lean.ts'
- 'etc/config/lean.*.properties'
- 'static/modes/lean-mode.ts'
'lang-llvm':
- changed-files:
- any-glob-to-any-file:

12
etc/config/lean.amazon.properties Normal file
View File

@@ -0,0 +1,12 @@
compilers=&lean
defaultCompiler=lean_4_29_1
compilerType=lean
supportsBinary=false
versionRe=^Lean \(version [^\n]+
group.lean.compilers=lean_4_29_1
group.lean.isSemVer=true
group.lean.baseName=Lean
compiler.lean_4_29_1.exe=/opt/compiler-explorer/lean-4.29.1/bin/lean
compiler.lean_4_29_1.semver=4.29.1

7
etc/config/lean.defaults.properties Normal file
View File

@@ -0,0 +1,7 @@
compilers=lean
compilerType=lean
supportsBinary=false
versionRe=^Lean \(version [^\n]+
compiler.lean.exe=lean
compiler.lean.name=Lean

4
examples/lean/default.lean Normal file
View File

@@ -0,0 +1,4 @@
def add (x y : Nat) : Nat := x + y
def main : IO Unit := do
IO.println (add 1 2)

29
lib/base-compiler.ts
View File

@@ -1655,6 +1655,10 @@ export class BaseCompiler {
return utils.changeExtension(inputFilename, '.dump-cmm');
}
getLeanCOutputFilename(outputFilename: string) {
return utils.changeExtension(outputFilename, '.c');
}
getYulOutputFilename(defaultOutputFilename: string) {
return utils.changeExtension(defaultOutputFilename, '.yul');
}
@@ -1737,6 +1741,25 @@ export class BaseCompiler {
return [{text: 'Internal error; unable to open output path'}];
}
async processLeanCOutput(
outputFilename: string,
output: CompilationResult,
options?: {['clang-format']: boolean} | null,
): Promise<ResultLine[]> {
if (output.code !== 0) {
return [{text: 'Failed to run compiler to get Lean C output'}];
}
const outpath = this.getLeanCOutputFilename(outputFilename);
if (await utils.fileExists(outpath)) {
let content = await fs.readFile(outpath, 'utf8');
if (options?.['clang-format']) {
content = await this.applyClangFormat(content);
}
return content.split('\n').map(line => ({text: line}));
}
return [{text: 'Internal error; unable to open output path'}];
}
async processYulOutput(
defaultOutputFilename: string,
result: CompilationResult,
@@ -2507,6 +2530,7 @@ export class BaseCompiler {
const makeHaskellCore = backendOptions.produceHaskellCore && this.compiler.supportsHaskellCoreView;
const makeHaskellStg = backendOptions.produceHaskellStg && this.compiler.supportsHaskellStgView;
const makeHaskellCmm = backendOptions.produceHaskellCmm && this.compiler.supportsHaskellCmmView;
const makeLeanC = !!backendOptions.produceLeanC && this.compiler.supportsLeanCView;
const makeGccDump = backendOptions.produceGccDump?.opened && this.compiler.supportsGccDump;
const makeYul = backendOptions.produceYul && this.compiler.supportsYulView;
@@ -2575,6 +2599,10 @@ export class BaseCompiler {
? await this.processHaskellExtraOutput(this.getHaskellCmmOutputFilename(inputFilename), asmResult)
: undefined;
const leanCResult = makeLeanC
? await this.processLeanCOutput(outputFilename, asmResult, backendOptions.produceLeanC)
: undefined;
const yulResult = makeYul
? await this.processYulOutput(outputFilename, asmResult, backendOptions.produceYul)
: undefined;
@@ -2628,6 +2656,7 @@ export class BaseCompiler {
asmResult.haskellCoreOutput = haskellCoreResult;
asmResult.haskellStgOutput = haskellStgResult;
asmResult.haskellCmmOutput = haskellCmmResult;
asmResult.leanCOutput = leanCResult;
asmResult.clojureMacroExpOutput = clojureMacroExpResult;

1
lib/compilers/_all.ts
View File

@@ -103,6 +103,7 @@ export {JavaCompiler} from './java.js';
export {JuliaCompiler} from './julia.js';
export {KotlinCompiler} from './kotlin.js';
export {LDCCompiler} from './ldc.js';
export {LeanCompiler} from './lean.js';
export {LFortranCompiler} from './lfortran.js';
export {LLCCompiler} from './llc.js';
export {LLVMmcaTool} from './llvm-mca.js';

167
lib/compilers/lean.ts Normal file
View File

@@ -0,0 +1,167 @@
// Copyright (c) 2026, 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 HOLDERS 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.
import path from 'node:path';
import {CompilationResult, ExecutionOptionsWithEnv} from '../../types/compilation/compilation.interfaces.js';
import type {PreliminaryCompilerInfo} from '../../types/compiler.interfaces.js';
import type {ParseFiltersAndOutputOptions} from '../../types/features/filters.interfaces.js';
import {BaseCompiler} from '../base-compiler.js';
import {CompilationEnvironment} from '../compilation-env.js';
export class LeanCompiler extends BaseCompiler {
// Flags that will be forwarded to `lean` instead of `leanc`.
private readonly leanFlags = new Set(['--profile', '--stats']);
static get key() {
return 'lean';
}
constructor(info: PreliminaryCompilerInfo, env: CompilationEnvironment) {
super(info, env);
this.compiler.supportsLeanCView = true;
}
override optionsForFilter(filters: ParseFiltersAndOutputOptions, outputFilename: string) {
return [`--c=${this.getLeanCOutputFilename(outputFilename)}`];
}
override getSharedLibraryPathsAsArguments() {
return [];
}
private async getLeanPrefix(compiler: string, execOptions: ExecutionOptionsWithEnv): Promise<string | null> {
const prefixResult = await this.exec(compiler, ['--print-prefix'], execOptions);
const prefix = prefixResult.stdout.trim();
if (prefixResult.code === 0 && prefix) {
return prefix;
}
return null;
}
private async getLeancPath(compiler: string, execOptions: ExecutionOptionsWithEnv): Promise<string> {
const prefix = await this.getLeanPrefix(compiler, execOptions);
if (prefix) return path.join(prefix, 'bin', 'leanc');
return path.join(path.dirname(compiler), 'leanc');
}
private async doLeanBuildstep(
command: string,
args: string[],
execOptions: ExecutionOptionsWithEnv,
inputFilename: string,
) {
const result = await this.exec(command, args, execOptions);
const processedResult = this.processExecutionResult(result, result.filenameTransform(inputFilename));
for (const output of [processedResult.stdout, processedResult.stderr]) {
for (const line of output) {
if (line.tag?.column !== undefined) {
// Lean reports zero-based columns, Monaco diagnostics use one-based columns
line.tag.column++;
}
}
}
return processedResult;
}
private partitionOptionsForSteps(
options: string[],
inputFilename: string,
): {
leanOptions: string[];
leancOptions: string[];
} {
const leanOptions: string[] = [];
const leancOptions: string[] = [];
for (let i = 0; i < options.length; i++) {
const option = options[i];
if (option.startsWith('--c=')) {
leanOptions.push(option);
} else if (option === inputFilename) {
leanOptions.push(option);
} else if (this.leanFlags.has(option)) {
leanOptions.push(option);
} else {
leancOptions.push(option);
}
}
return {leanOptions, leancOptions};
}
override async runCompiler(
compiler: string,
options: string[],
inputFilename: string,
execOptions: ExecutionOptionsWithEnv,
): Promise<CompilationResult> {
if (!execOptions) {
execOptions = this.getDefaultExecOptions();
}
const tmpDir = path.dirname(inputFilename);
if (!execOptions.customCwd) {
execOptions.customCwd = tmpDir;
}
const outputFilename = this.getOutputFilename(tmpDir, this.outputFilebase);
const cOutputOption = options.find(option => option.startsWith('--c='));
const cOutputFilename = cOutputOption?.substring('--c='.length) || this.getLeanCOutputFilename(outputFilename);
const {leanOptions, leancOptions} = this.partitionOptionsForSteps(options, inputFilename);
const leanResult = await this.doLeanBuildstep(compiler, leanOptions, execOptions, inputFilename);
if (leanResult.code !== 0) {
return {
...leanResult,
inputFilename,
languageId: 'asm',
};
}
const leanc = await this.getLeancPath(compiler, execOptions);
const leancResult = await this.doBuildstep(
leanc,
[...leancOptions, '-S', cOutputFilename, '-o', outputFilename],
execOptions,
);
return {
...leancResult,
okToCache: leanResult.okToCache && leancResult.okToCache,
stdout: leanResult.stdout.concat(leancResult.stdout),
stderr: leanResult.stderr.concat(leancResult.stderr),
inputFilename,
languageId: 'asm',
};
}
}

12
lib/languages.ts
View File

@@ -584,6 +584,18 @@ const definitions: Record<LanguageKey, LanguageDefinition> = {
monacoDisassembly: null,
digitSeparator: '_',
},
lean: {
name: 'Lean',
monaco: 'lean',
extensions: ['.lean'],
alias: [],
logoFilename: 'lean.png',
logoFilenameDark: null,
formatter: null,
previewFilter: null,
monacoDisassembly: null,
digitSeparator: '_',
},
llvm: {
name: 'LLVM IR',
monaco: 'llvm-ir',

BIN
public/logos/lean.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 6.1 KiB

12
static/components.interfaces.ts
View File

@@ -27,6 +27,7 @@ import GoldenLayout from 'golden-layout';
import {ConfiguredOverrides} from '../types/compilation/compiler-overrides.interfaces.js';
import {ConfiguredRuntimeTools} from '../types/execution/execution.interfaces.js';
import {CompilerOutputOptions} from '../types/features/filters.interfaces.js';
import {ResultLine} from '../types/resultline/resultline.interfaces.js';
import {CfgState} from './panes/cfg-view.interfaces.js';
import {ClangirState} from './panes/clangir-view.interfaces.js';
import {GccDumpViewState} from './panes/gccdump-view.interfaces.js';
@@ -71,6 +72,7 @@ export const RUST_MIR_VIEW_COMPONENT_NAME = 'rustmir' as const;
export const HASKELL_CORE_VIEW_COMPONENT_NAME = 'haskellCore' as const;
export const HASKELL_STG_VIEW_COMPONENT_NAME = 'haskellStg' as const;
export const HASKELL_CMM_VIEW_COMPONENT_NAME = 'haskellCmm' as const;
export const LEAN_C_VIEW_COMPONENT_NAME = 'leanC' as const;
export const GNAT_DEBUG_TREE_VIEW_COMPONENT_NAME = 'gnatdebugtree' as const;
export const GNAT_DEBUG_VIEW_COMPONENT_NAME = 'gnatdebug' as const;
export const RUST_MACRO_EXP_VIEW_COMPONENT_NAME = 'rustmacroexp' as const;
@@ -297,6 +299,15 @@ export type PopulatedHaskellCmmViewState = StateWithId & {
treeid: number;
};
export type EmptyLeanCViewState = EmptyState;
export type PopulatedLeanCViewState = StateWithId & {
source: string;
leanCOutput: ResultLine[];
compilerName: string;
editorid: number;
treeid: number;
};
export type EmptyGnatDebugTreeViewState = EmptyState;
export type PopulatedGnatDebugTreeViewState = StateWithId & {
source: string;
@@ -396,6 +407,7 @@ export interface ComponentStateMap {
[HASKELL_CORE_VIEW_COMPONENT_NAME]: EmptyHaskellCoreViewState | PopulatedHaskellCoreViewState;
[HASKELL_STG_VIEW_COMPONENT_NAME]: EmptyHaskellStgViewState | PopulatedHaskellStgViewState;
[HASKELL_CMM_VIEW_COMPONENT_NAME]: EmptyHaskellCmmViewState | PopulatedHaskellCmmViewState;
[LEAN_C_VIEW_COMPONENT_NAME]: EmptyLeanCViewState | PopulatedLeanCViewState;
[GNAT_DEBUG_TREE_VIEW_COMPONENT_NAME]: EmptyGnatDebugTreeViewState | PopulatedGnatDebugTreeViewState;
[GNAT_DEBUG_VIEW_COMPONENT_NAME]: EmptyGnatDebugViewState | PopulatedGnatDebugViewState;
[RUST_MACRO_EXP_VIEW_COMPONENT_NAME]: EmptyRustMacroExpViewState | PopulatedRustMacroExpViewState;

34
static/components.ts
View File

@@ -28,6 +28,7 @@ import {ConfiguredOverrides} from '../types/compilation/compiler-overrides.inter
import {ConfiguredRuntimeTools} from '../types/execution/execution.interfaces.js';
import {ParseFiltersAndOutputOptions} from '../types/features/filters.interfaces.js';
import {LanguageKey} from '../types/languages.interfaces.js';
import {ResultLine} from '../types/resultline/resultline.interfaces.js';
import {
AnyComponentConfig,
AST_VIEW_COMPONENT_NAME,
@@ -55,6 +56,7 @@ import {
IR_VIEW_COMPONENT_NAME,
ItemConfig,
LayoutItem,
LEAN_C_VIEW_COMPONENT_NAME,
LLVM_OPT_PIPELINE_VIEW_COMPONENT_NAME,
OPT_PIPELINE_VIEW_COMPONENT_NAME,
OPT_VIEW_COMPONENT_NAME,
@@ -816,6 +818,38 @@ export function getYulViewWith(
};
}
/** Get an empty Lean C view component. */
export function getLeanCView(): ComponentConfig<typeof LEAN_C_VIEW_COMPONENT_NAME> {
return {
type: 'component',
componentName: LEAN_C_VIEW_COMPONENT_NAME,
componentState: {},
};
}
/** Get a Lean C view with the given configuration. */
export function getLeanCViewWith(
id: number,
source: string,
leanCOutput: ResultLine[] | undefined,
compilerName: string,
editorid: number,
treeid: number,
): ComponentConfig<typeof LEAN_C_VIEW_COMPONENT_NAME> {
return {
type: 'component',
componentName: LEAN_C_VIEW_COMPONENT_NAME,
componentState: {
id,
source,
leanCOutput,
compilerName,
editorid,
treeid,
},
};
}
/** Get an empty gnat debug tree view component. */
export function getGnatDebugTreeView(): ComponentConfig<typeof GNAT_DEBUG_TREE_VIEW_COMPONENT_NAME> {
return {

4
static/event-map.ts
View File

@@ -35,6 +35,7 @@ import {MessageWithLocation} from '../types/resultline/resultline.interfaces.js'
import {NewToolSettings, ToolState} from './components.interfaces.js';
import {Motd} from './motd.interfaces.js';
import {GccDumpFiltersState, GccDumpViewSelectedPass} from './panes/gccdump-view.interfaces.js';
import {LeanCOptions} from './panes/leanc-view.interfaces.js';
import {PPOptions} from './panes/pp-view.interfaces.js';
import {SiteSettings} from './settings.js';
import {Theme} from './themes.js';
@@ -114,6 +115,9 @@ export type EventMap = {
haskellCoreViewOpened: (compilerId: number) => void;
haskellStgViewClosed: (compilerId: number) => void;
haskellStgViewOpened: (compilerId: number) => void;
leanCViewClosed: (compilerId: number) => void;
leanCViewOpened: (compilerId: number) => void;
leanCViewOptionsUpdated: (compilerId: number, options: LeanCOptions, recompile: boolean) => void;
initialised: () => void;
irViewClosed: (compilerId: number) => void;
irViewOpened: (compilerId: number) => void;

7
static/hub.ts
View File

@@ -48,6 +48,7 @@ import {
HASKELL_STG_VIEW_COMPONENT_NAME,
InferComponentState,
IR_VIEW_COMPONENT_NAME,
LEAN_C_VIEW_COMPONENT_NAME,
LLVM_OPT_PIPELINE_VIEW_COMPONENT_NAME,
OPT_PIPELINE_VIEW_COMPONENT_NAME,
OPT_VIEW_COMPONENT_NAME,
@@ -84,6 +85,7 @@ import {HaskellCmm as HaskellCmmView} from './panes/haskellcmm-view.js';
import {HaskellCore as HaskellCoreView} from './panes/haskellcore-view.js';
import {HaskellStg as HaskellStgView} from './panes/haskellstg-view.js';
import {Ir as IrView} from './panes/ir-view.js';
import {LeanC as LeanCView} from './panes/leanc-view.js';
import {OptPipeline} from './panes/opt-pipeline.js';
import {Opt as OptView} from './panes/opt-view.js';
import {Output} from './panes/output.js';
@@ -159,6 +161,7 @@ export class Hub {
);
layout.registerComponent(HASKELL_STG_VIEW_COMPONENT_NAME, (c: GLC, s: any) => this.haskellStgViewFactory(c, s));
layout.registerComponent(HASKELL_CMM_VIEW_COMPONENT_NAME, (c: GLC, s: any) => this.haskellCmmViewFactory(c, s));
layout.registerComponent(LEAN_C_VIEW_COMPONENT_NAME, (c: GLC, s: any) => this.leanCViewFactory(c, s));
layout.registerComponent(GNAT_DEBUG_TREE_VIEW_COMPONENT_NAME, (c: GLC, s: any) =>
this.gnatDebugTreeViewFactory(c, s),
);
@@ -583,6 +586,10 @@ export class Hub {
return new HaskellCmmView(this, container, state);
}
public leanCViewFactory(container: GoldenLayout.Container, state: InferComponentState<LeanCView>): LeanCView {
return new LeanCView(this, container, state);
}
public clojureMacroExpViewFactory(
container: GoldenLayout.Container,
state: InferComponentState<ClojureMacroExpView>,

1
static/modes/_all.ts
View File

@@ -52,6 +52,7 @@ import './hook-mode';
import './hylo-mode';
import './ispc-mode';
import './jakt-mode';
import './lean-mode';
import './llvm-ir-mode';
import './mlir-mode';
import './modula2-mode';

347
static/modes/lean-mode.ts Normal file
View File

@@ -0,0 +1,347 @@
// Copyright (c) 2026, 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.
import * as monaco from 'monaco-editor';
// Based on https://github.com/leanprover/vscode-lean4/blob/bbe3ff12/vscode-lean4/syntaxes/lean4.json.
function definition(): monaco.languages.IMonarchLanguage {
return {
escapes: /\\(?:[\\'"ntr]|x[0-9A-Fa-f]{2}|u[0-9A-Fa-f]{4})/,
keywords: [
'local',
'scoped',
'partial',
'unsafe',
'nonrec',
'public',
'private',
'protected',
'noncomputable',
'meta',
'deriving',
'instance',
'inductive',
'coinductive',
'structure',
'theorem',
'axiom',
'abbrev',
'lemma',
'def',
'instance',
'class',
'with',
'extends',
'where',
'theorem',
'show',
'have',
'using',
'haveI',
'from',
'suffices',
'nomatch',
'nofun',
'no_index',
'def',
'class',
'structure',
'instance',
'elab',
'set_option',
'initialize',
'builtin_initialize',
'example',
'inductive_fixpoint',
'inductive',
'coinductive_fixpoint',
'coinductive',
'termination_by?',
'termination_by',
'decreasing_by',
'partial_fixpoint',
'axiom',
'universe',
'variable',
'module',
'import all',
'import',
'open',
'export',
'prelude',
'renaming',
'hiding',
'do',
'by?',
'by',
'let',
'letI',
'let_expr',
'extends',
'mutual',
'mut',
'where',
'rec',
'declare_syntax_cat',
'syntax',
'macro_rules',
'macro',
'max_prec',
'leading_parser',
'elab_rules',
'deriving',
'fun',
'section',
'namespace',
'end',
'prefix',
'postfix',
'infixl',
'infixr',
'infix',
'notation',
'abbrev',
'if',
'bif',
'then',
'else',
'calc',
'matches',
'match_expr',
'match',
'with',
'forall',
'for',
'while',
'repeat',
'unless',
'until',
'panic!',
'unreachable!',
'assert!',
'try',
'catch',
'finally',
'return',
'continue',
'break',
'exists',
'mod_cast',
'include_str',
'include',
'in',
'trailing_parser',
'tactic_tag',
'tactic_alt',
'tactic_extension',
'register_tactic_tag',
'binder_predicate',
'grind_propagator',
'builtin_grind_propagator',
'grind_pattern',
'simproc',
'builtin_simproc',
'simproc_decl',
'builtin_simproc_decl',
'dsimproc',
'builtin_dsimproc',
'dsimproc_decl',
'builtin_dsimproc_decl',
'show_panel_widgets',
'show_term',
'seal',
'unseal',
'nat_lit',
'norm_cast_add_elim',
'println!',
'declare_config_elab',
'register_error_explanation',
'register_builtin_option',
'register_option',
'register_parser_alias',
'register_simp_attr',
'register_linter_set',
'register_label_attr',
'recommended_spelling',
'reportIssue!',
'reprove',
'run_elab',
'run_cmd',
'run_meta',
'add_decl_doc',
'omit',
'opaque',
'dbg_trace',
'trace_goal',
'trace',
'throwErrorAt',
'throwError',
'throwNamedErrorAt',
'throwNamedError',
'logNamedWarningAt',
'logNamedWarning',
'logNamedErrorAt',
'logNamedError',
],
types: ['Prop', 'Type', 'Sort'],
invalidKeywords: ['sorry', 'admit'],
commands: [
'#print',
'#eval',
'#eval!',
'#reduce',
'#synth',
'#widget',
'#where',
'#version',
'#with_exporting',
'#check',
'#check_tactic',
'#check_tactic_failure',
'#check_failure',
'#check_simp',
'#discr_tree_key',
'#discr_tree_simp_key',
'#guard',
'#guard_expr',
'#guard_msgs',
],
invalidCommands: ['#exit'],
tokenizer: {
root: [
[/r(#*)"/, {token: 'string.quote', bracket: '@open', next: '@stringraw.$1'}],
{include: '@whitespace'},
[/"/, 'string', '@string'],
[/(?<![\]\w])'[^\\']'/, 'string'],
[/(?<![\]\w])(')(@escapes)(')/, ['string', 'string.escape', 'string']],
[/\b(0[xX][0-9a-fA-F]+|[0-9]+|-?(0|[1-9][0-9]*)(\.[0-9]+)?([eE][+-]?[0-9]+)?)\b/, 'number'],
[/«/, 'identifier', '@escapedIdentifier'],
[/\battribute\b\s*\[[^\]\s]*\]/, 'keyword.modifier'],
[/@\[[^\]\s]*\]/, 'keyword.modifier'],
[
/#[a-zA-Z_][a-zA-Z0-9_!]*/,
{
cases: {
'@invalidCommands': 'invalid',
'@commands': 'keyword',
'@default': '',
},
},
],
[/[{}()[\]]/, '@brackets'],
[
/[a-zA-Z_][a-zA-Z0-9_'?!]*/,
{
cases: {
'@invalidKeywords': 'invalid',
'@keywords': 'keyword',
'@types': 'keyword.type',
'@default': 'identifier',
},
},
],
],
whitespace: [
[/[ \t\r\n]+/, 'white'],
[/--.*$/, 'comment'],
[/\/--/, 'comment.doc', '@docComment'],
[/\/-!/, 'comment.doc', '@docComment'],
[/\/-/, 'comment', '@blockComment'],
],
docComment: [
[/[^/-]+/, 'comment.doc'],
[/\/-/, 'comment.doc', '@blockComment'],
[/-\//, 'comment.doc', '@pop'],
[/[/-]/, 'comment.doc'],
],
blockComment: [
[/[^/-]+/, 'comment'],
[/\/-/, 'comment', '@push'],
[/-\//, 'comment', '@pop'],
[/[/-]/, 'comment'],
],
string: [
[/[^\\"]+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/"/, 'string', '@pop'],
],
escapedIdentifier: [
[/[^»]+/, 'identifier'],
[/»/, 'identifier', '@pop'],
],
stringraw: [
[/[^"#]+/, {token: 'string'}],
[
/"(#*)/,
{
cases: {
'$1==$S2': {token: 'string.quote', bracket: '@close', next: '@pop'},
'@default': {token: 'string'},
},
},
],
[/["#]/, {token: 'string'}],
],
},
};
}
monaco.languages.register({id: 'lean'});
monaco.languages.setMonarchTokensProvider('lean', definition());
monaco.languages.setLanguageConfiguration('lean', {
comments: {
lineComment: '--',
blockComment: ['/-', '-/'],
},
brackets: [
['(', ')'],
['[', ']'],
['{', '}'],
],
autoClosingPairs: [
{open: '(', close: ')'},
{open: '[', close: ']'},
{open: '{', close: '}'},
{open: '"', close: '"', notIn: ['string', 'comment']},
],
surroundingPairs: [
{open: '(', close: ')'},
{open: '[', close: ']'},
{open: '{', close: '}'},
{open: '"', close: '"'},
],
});

57
static/panes/compiler.ts
View File

@@ -66,6 +66,7 @@ import * as TimingWidget from '../widgets/timing-info-widget.js';
import {Toggles} from '../widgets/toggles.js';
import {CompilerCurrentState, CompilerState} from './compiler.interfaces.js';
import {GccDumpFiltersState, GccDumpViewSelectedPass} from './gccdump-view.interfaces.js';
import {LeanCOptions} from './leanc-view.interfaces.js';
import {MonacoPaneState} from './pane.interfaces.js';
import {MonacoPane} from './pane.js';
import {PPOptions} from './pp-view.interfaces.js';
@@ -197,6 +198,7 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
private haskellCoreButton: JQuery<HTMLButtonElement>;
private haskellStgButton: JQuery<HTMLButtonElement>;
private haskellCmmButton: JQuery<HTMLButtonElement>;
private leanCButton: JQuery<HTMLButtonElement>;
private clojureMacroExpButton: JQuery<HTMLButtonElement>;
private yulButton: JQuery<HTMLButtonElement>;
private gccDumpButton: JQuery<HTMLButtonElement>;
@@ -276,6 +278,8 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
private haskellCoreViewOpen: boolean;
private haskellStgViewOpen: boolean;
private haskellCmmViewOpen: boolean;
private leanCViewOpen: boolean;
private leanCOptions: LeanCOptions;
private clojureMacroExpViewOpen: boolean;
private yulViewOpen: boolean;
private ppOptions: PPOptions;
@@ -633,6 +637,17 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
);
};
const createLeanCView = () => {
return Components.getLeanCViewWith(
this.id,
this.source,
this.lastResult?.leanCOutput,
this.getCompilerName(),
this.sourceEditorId ?? 0,
this.sourceTreeId ?? 0,
);
};
const createClojureMacroExpView = () => {
return Components.getClojureMacroExpViewWith(
this.id,
@@ -904,6 +919,18 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
insertPoint.addChild(createHaskellCmmView());
});
createDragSource(this.container.layoutManager, this.leanCButton, () => createLeanCView()).on(
'dragStart',
hidePaneAdder,
);
this.leanCButton.on('click', () => {
const insertPoint =
this.hub.findParentRowOrColumn(this.container.parent) ||
this.container.layoutManager.root.contentItems[0];
insertPoint.addChild(createLeanCView());
});
createDragSource(this.container.layoutManager, this.rustMacroExpButton, () => createRustMacroExpView()).on(
'dragStart',
hidePaneAdder,
@@ -1346,6 +1373,7 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
produceHaskellCore: this.haskellCoreViewOpen,
produceHaskellStg: this.haskellStgViewOpen,
produceHaskellCmm: this.haskellCmmViewOpen,
produceLeanC: this.leanCViewOpen ? this.leanCOptions : null,
produceClojureMacroExp: this.clojureMacroExpViewOpen,
produceYul: this.yulViewOpen ? this.yulOptions : null,
overrides: this.getCurrentState().overrides,
@@ -2216,6 +2244,29 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
}
}
onLeanCViewOpened(id: number): void {
if (this.id === id) {
this.leanCButton.prop('disabled', true);
this.leanCViewOpen = true;
}
}
onLeanCViewClosed(id: number): void {
if (this.id === id) {
this.leanCButton.prop('disabled', false);
this.leanCViewOpen = false;
}
}
onLeanCViewOptionsUpdated(id: number, options: LeanCOptions, recompile: boolean): void {
if (this.id === id) {
this.leanCOptions = options;
if (recompile) {
this.compile();
}
}
}
onGnatDebugTreeViewOpened(id: number): void {
if (this.id === id) {
this.gnatDebugTreeButton.prop('disabled', true);
@@ -2503,6 +2554,7 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
this.haskellCoreButton = this.domRoot.find('.btn.view-haskellCore');
this.haskellStgButton = this.domRoot.find('.btn.view-haskellStg');
this.haskellCmmButton = this.domRoot.find('.btn.view-haskellCmm');
this.leanCButton = this.domRoot.find('.btn.view-leanC');
this.clojureMacroExpButton = this.domRoot.find('.btn.view-clojuremacroexp');
this.yulButton = this.domRoot.find('.btn.view-yul');
this.gccDumpButton = this.domRoot.find('.btn.view-gccdump');
@@ -2794,6 +2846,7 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
this.haskellCoreButton.prop('disabled', this.haskellCoreViewOpen);
this.haskellStgButton.prop('disabled', this.haskellStgViewOpen);
this.haskellCmmButton.prop('disabled', this.haskellCmmViewOpen);
this.leanCButton.prop('disabled', this.leanCViewOpen);
this.rustMacroExpButton.prop('disabled', this.rustMacroExpViewOpen);
this.rustHirButton.prop('disabled', this.rustHirViewOpen);
this.clojureMacroExpButton.prop('disabled', this.clojureMacroExpViewOpen);
@@ -2818,6 +2871,7 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
this.haskellCoreButton.toggle(!!this.compiler.supportsHaskellCoreView);
this.haskellStgButton.toggle(!!this.compiler.supportsHaskellStgView);
this.haskellCmmButton.toggle(!!this.compiler.supportsHaskellCmmView);
this.leanCButton.toggle(!!this.compiler.supportsLeanCView);
this.clojureMacroExpButton.toggle(!!this.compiler.supportsClojureMacroExpView);
this.yulButton.toggle(!!this.compiler.supportsYulView);
// TODO(jeremy-rifkin): Disable cfg button when binary mode is set?
@@ -3000,6 +3054,9 @@ export class Compiler extends MonacoPane<monaco.editor.IStandaloneCodeEditor, Co
this.eventHub.on('haskellStgViewClosed', this.onHaskellStgViewClosed, this);
this.eventHub.on('haskellCmmViewOpened', this.onHaskellCmmViewOpened, this);
this.eventHub.on('haskellCmmViewClosed', this.onHaskellCmmViewClosed, this);
this.eventHub.on('leanCViewOpened', this.onLeanCViewOpened, this);
this.eventHub.on('leanCViewClosed', this.onLeanCViewClosed, this);
this.eventHub.on('leanCViewOptionsUpdated', this.onLeanCViewOptionsUpdated, this);
this.eventHub.on('clojureMacroExpViewOpened', this.onClojureMacroExpViewOpened, this);
this.eventHub.on('clojureMacroExpViewClosed', this.onClojureMacroExpViewClosed, this);
this.eventHub.on('yulViewOpened', this.onYulViewOpened, this);

1
static/panes/diff.interfaces.ts
View File

@@ -39,6 +39,7 @@ export enum DiffType {
RustHirOutput = 12,
ClojureMacroExpOutput = 13,
YulOutput = 14,
LeanCOutput = 15,
}
export type DiffState = {

8
static/panes/diff.ts
View File

@@ -181,6 +181,11 @@ class DiffStateObject {
{text: "<select 'Add new...' → 'Yul (Solidity IR)' in this compiler's pane>"},
];
break;
case DiffType.LeanCOutput:
output = this.result.leanCOutput || [
{text: "<select 'Add new...' → 'Lean C Output' in this compiler's pane>"},
];
break;
}
}
this.model.setValue(output.map(x => x.text).join('\n'));
@@ -490,6 +495,9 @@ export class Diff extends MonacoPane<monaco.editor.IStandaloneDiffEditor, DiffSt
if (compiler.supportsYulView) {
options.push({id: DiffType.YulOutput.toString(), name: 'Yul (Solidity IR)'});
}
if (compiler.supportsLeanCView) {
options.push({id: DiffType.LeanCOutput.toString(), name: 'Lean C Output'});
}
}
const lhsoptions = this.getDiffableOptions(this.selectize.lhs, lhsextraoptions);

31
static/panes/leanc-view.interfaces.ts Normal file
View File

@@ -0,0 +1,31 @@
// Copyright (c) 2026, 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 HOLDERS 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.
import {ResultLine} from '../../types/resultline/resultline.interfaces.js';
export interface LeanCState {
leanCOutput: ResultLine[];
}
export type {LeanCOptions} from '../../types/compilation/lean-c.interfaces.js';

151
static/panes/leanc-view.ts Normal file
View File

@@ -0,0 +1,151 @@
// Copyright (c) 2026, 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 HOLDERS 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.
import {Container} from 'golden-layout';
import $ from 'jquery';
import * as monaco from 'monaco-editor';
import _ from 'underscore';
import {CompilationResult} from '../../types/compilation/compilation.interfaces.js';
import {CompilerInfo} from '../../types/compiler.interfaces.js';
import {Hub} from '../hub.js';
import {extendConfig} from '../monaco-config.js';
import {Toggles} from '../widgets/toggles.js';
import {LeanCOptions, LeanCState} from './leanc-view.interfaces.js';
import {MonacoPaneState} from './pane.interfaces.js';
import {MonacoPane} from './pane.js';
export class LeanC extends MonacoPane<monaco.editor.IStandaloneCodeEditor, LeanCState> {
private options: Toggles;
constructor(hub: Hub, container: Container, state: LeanCState & MonacoPaneState) {
super(hub, container, state);
if (state.leanCOutput) {
this.showLeanCResults(state.leanCOutput);
}
this.onOptionsChange();
}
override getInitialHTML(): string {
return $('#leanC').html();
}
override createEditor(editorRoot: HTMLElement): void {
this.editor = monaco.editor.create(
editorRoot,
extendConfig({
language: 'c',
readOnly: true,
glyphMargin: true,
lineNumbersMinChars: 3,
}),
);
}
override getPrintName() {
return 'Lean C Output';
}
override getDefaultPaneName(): string {
return 'Lean C Output';
}
override registerButtons(state: LeanCState & MonacoPaneState): void {
super.registerButtons(state);
this.options = new Toggles(this.domRoot.find('.options'), state as unknown as Record<string, boolean>);
this.options.on('change', this.onOptionsChange.bind(this));
}
override registerCallbacks(): void {
const throttleFunction = _.throttle(
(event: monaco.editor.ICursorSelectionChangedEvent) => this.onDidChangeCursorSelection(event),
500,
);
this.editor.onDidChangeCursorSelection(event => throttleFunction(event));
this.eventHub.emit('leanCViewOpened', this.compilerInfo.compilerId);
this.eventHub.emit('requestSettings');
}
override getCurrentState(): MonacoPaneState {
return {
...super.getCurrentState(),
...this.options.get(),
};
}
onOptionsChange(): void {
const options = this.options.get() as LeanCOptions;
this.updateState();
this.showLeanCResults([{text: '<Compiling...>'}]);
this.eventHub.emit('leanCViewOptionsUpdated', this.compilerInfo.compilerId, options, true);
}
override onCompileResult(compilerId: number, compiler: CompilerInfo, result: CompilationResult): void {
if (this.compilerInfo.compilerId !== compilerId) return;
if (result.leanCOutput) {
this.showLeanCResults(result.leanCOutput);
} else if (compiler.supportsLeanCView) {
this.showLeanCResults([{text: '<No output>'}]);
}
}
override onCompiler(
compilerId: number,
compiler: CompilerInfo | null,
options: string,
editorId?: number,
treeId?: number,
): void {
if (this.compilerInfo.compilerId === compilerId) {
this.compilerInfo.compilerName = compiler ? compiler.name : '';
this.compilerInfo.editorId = editorId;
this.compilerInfo.treeId = treeId;
this.updateTitle();
if (compiler && !compiler.supportsLeanCView) {
this.showLeanCResults([{text: '<Lean C output is not supported for this compiler>'}]);
}
}
}
showLeanCResults(result: Record<'text', string>[]): void {
this.editor
.getModel()
?.setValue(result.length ? _.pluck(result, 'text').join('\n') : '<No Lean C output generated>');
if (!this.isAwaitingInitialResults) {
if (this.selection) {
this.editor.setSelection(this.selection);
this.editor.revealLinesInCenter(this.selection.selectionStartLineNumber, this.selection.endLineNumber);
}
this.isAwaitingInitialResults = true;
}
}
override close(): void {
this.eventHub.unsubscribe();
this.eventHub.emit('leanCViewClosed', this.compilerInfo.compilerId);
this.editor.dispose();
}
}

3
types/compilation/compilation.interfaces.ts
View File

@@ -41,6 +41,7 @@ import {CFGResult} from './cfg.interfaces.js';
import {ClangirBackendOptions} from './clangir.interfaces.js';
import {ConfiguredOverrides} from './compiler-overrides.interfaces.js';
import {LLVMIrBackendOptions} from './ir.interfaces.js';
import type {LeanCOptions} from './lean-c.interfaces.js';
import {OptPipelineBackendOptions, OptPipelineOutput} from './opt-pipeline-output.interfaces.js';
import {YulBackendOptions} from './yul.interfaces.js';
@@ -117,6 +118,7 @@ export type CompilationRequestOptions = {
produceHaskellCore?: boolean;
produceHaskellStg?: boolean;
produceHaskellCmm?: boolean;
produceLeanC?: LeanCOptions | null;
produceClojureMacroExp?: boolean;
produceYul?: YulBackendOptions | null;
cmakeArgs?: string;
@@ -216,6 +218,7 @@ export type CompilationResult = {
haskellCoreOutput?: ResultLine[];
haskellStgOutput?: ResultLine[];
haskellCmmOutput?: ResultLine[];
leanCOutput?: ResultLine[];
clojureMacroExpOutput?: ResultLine[];

27
types/compilation/lean-c.interfaces.ts Normal file
View File

@@ -0,0 +1,27 @@
// Copyright (c) 2026, 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.
export type LeanCOptions = {
'clang-format': boolean;
};

1
types/compiler.interfaces.ts
View File

@@ -103,6 +103,7 @@ export type CompilerInfo = {
supportsHaskellCoreView?: boolean;
supportsHaskellStgView?: boolean;
supportsHaskellCmmView?: boolean;
supportsLeanCView?: boolean;
supportsClojureMacroExpView?: boolean;
supportsYulView?: boolean;
supportsCfg?: boolean;

1
types/languages.interfaces.ts
View File

@@ -72,6 +72,7 @@ export type LanguageKey =
| 'julia'
| 'javascript'
| 'kotlin'
| 'lean'
| 'llvm'
| 'llvm_mir'
| 'mlir'

1
views/templates/panes/compiler.pug
View File

@@ -64,6 +64,7 @@ mixin newPaneButton(classId, text, title, icon)
+newPaneButton("view-haskellCore", "GHC Core", "Show GHC Core Intermediate Representation", "fas fa-water")
+newPaneButton("view-haskellStg", "GHC STG", "Show GHC STG Intermediate Representation", "fas fa-water")
+newPaneButton("view-haskellCmm", "GHC Cmm", "Show GHC Cmm Intermediate Representation", "fas fa-water")
+newPaneButton("view-leanC", "Lean C Output", "Show generated Lean C output", "fas fa-align-center")
+newPaneButton("view-clojuremacroexp", "Clojure Macro Expansion", "Show Clojure macro expansion", "fas fa-arrows-alt")
+newPaneButton("view-yul", "Yul (Solidity IR)", "Show Solidity Intermediate Representation", "fas fa-align-center")
+newPaneButton("view-gccdump", "GCC Tree/RTL", "Show GCC Tree/RTL dump", "fas fa-tree")

10
views/templates/panes/leanc.pug Normal file
View File

@@ -0,0 +1,10 @@
#leanC
.top-bar.btn-toolbar.bg-light(role="toolbar")
include ../../font-size
.btn-group.btn-group-sm.options(role="group" aria-label="Panel options")
.input-group.input-group-sm.mb-auto
.button-checkbox
button.btn.btn-sm.btn-light.clang-format(type="button" title="Apply clang-format to output" data-bind="clang-format" aria-pressed="true" aria-label="Apply clang-format")
span Apply clang-format
input.d-none(type="checkbox" checked=true)
.monaco-placeholder

2
views/templates/templates.pug
View File

@@ -20,6 +20,8 @@ mixin monacopane(id)
include panes/pp
include panes/leanc
include panes/ir
include panes/clangir