diff --git a/.github/labeler.yml b/.github/labeler.yml index 3d3936f0d..e84ddea93 100644 --- a/.github/labeler.yml +++ b/.github/labeler.yml @@ -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: diff --git a/etc/config/lean.amazon.properties b/etc/config/lean.amazon.properties new file mode 100644 index 000000000..0755571e1 --- /dev/null +++ b/etc/config/lean.amazon.properties @@ -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 diff --git a/etc/config/lean.defaults.properties b/etc/config/lean.defaults.properties new file mode 100644 index 000000000..05a7fa1e5 --- /dev/null +++ b/etc/config/lean.defaults.properties @@ -0,0 +1,7 @@ +compilers=lean +compilerType=lean +supportsBinary=false +versionRe=^Lean \(version [^\n]+ + +compiler.lean.exe=lean +compiler.lean.name=Lean diff --git a/examples/lean/default.lean b/examples/lean/default.lean new file mode 100644 index 000000000..7ed2624b4 --- /dev/null +++ b/examples/lean/default.lean @@ -0,0 +1,4 @@ +def add (x y : Nat) : Nat := x + y + +def main : IO Unit := do + IO.println (add 1 2) diff --git a/lib/base-compiler.ts b/lib/base-compiler.ts index 8ba4af6c6..359ff954f 100644 --- a/lib/base-compiler.ts +++ b/lib/base-compiler.ts @@ -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 { + 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; diff --git a/lib/compilers/_all.ts b/lib/compilers/_all.ts index 46325641f..7d355be55 100644 --- a/lib/compilers/_all.ts +++ b/lib/compilers/_all.ts @@ -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'; diff --git a/lib/compilers/lean.ts b/lib/compilers/lean.ts new file mode 100644 index 000000000..cd330bb81 --- /dev/null +++ b/lib/compilers/lean.ts @@ -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 { + 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 { + 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 { + 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', + }; + } +} diff --git a/lib/languages.ts b/lib/languages.ts index 079e7809f..aa9e5f66e 100644 --- a/lib/languages.ts +++ b/lib/languages.ts @@ -584,6 +584,18 @@ const definitions: Record = { 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', diff --git a/public/logos/lean.png b/public/logos/lean.png new file mode 100644 index 000000000..3882eed6f Binary files /dev/null and b/public/logos/lean.png differ diff --git a/static/components.interfaces.ts b/static/components.interfaces.ts index e605450f1..cf3b0b095 100644 --- a/static/components.interfaces.ts +++ b/static/components.interfaces.ts @@ -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; diff --git a/static/components.ts b/static/components.ts index 6d7312665..931775c68 100644 --- a/static/components.ts +++ b/static/components.ts @@ -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 { + 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 { + 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 { return { diff --git a/static/event-map.ts b/static/event-map.ts index 138e82d80..5dde3f187 100644 --- a/static/event-map.ts +++ b/static/event-map.ts @@ -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; diff --git a/static/hub.ts b/static/hub.ts index 15f66e0f7..23b467ad1 100644 --- a/static/hub.ts +++ b/static/hub.ts @@ -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 { + return new LeanCView(this, container, state); + } + public clojureMacroExpViewFactory( container: GoldenLayout.Container, state: InferComponentState, diff --git a/static/modes/_all.ts b/static/modes/_all.ts index 5f0577572..d6c3a1c24 100644 --- a/static/modes/_all.ts +++ b/static/modes/_all.ts @@ -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'; diff --git a/static/modes/lean-mode.ts b/static/modes/lean-mode.ts new file mode 100644 index 000000000..5604ba219 --- /dev/null +++ b/static/modes/lean-mode.ts @@ -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'], + [/(?; private haskellStgButton: JQuery; private haskellCmmButton: JQuery; + private leanCButton: JQuery; private clojureMacroExpButton: JQuery; private yulButton: JQuery; private gccDumpButton: JQuery; @@ -276,6 +278,8 @@ export class Compiler extends MonacoPane { + 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 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"}, ]; break; + case DiffType.LeanCOutput: + output = this.result.leanCOutput || [ + {text: "