Skip to content

Add Lean 4 Lang - #2714

Open
Bubbler-4 wants to merge 17 commits into
code-golf:masterfrom
Bubbler-4:add-lean
Open

Add Lean 4 Lang#2714
Bubbler-4 wants to merge 17 commits into
code-golf:masterfrom
Bubbler-4:add-lean

Conversation

@Bubbler-4

@Bubbler-4 Bubbler-4 commented Aug 12, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Implements #2702

Notes:

  • The language name is set to Lean
  • The entire release is downloaded, unzipped, and put verbatim in the container at /usr/local/lean/
    • The unzipped size is ~3GB, but there's no quick win to shave it off (other than stripping .so files maybe; many giant files are .olean and .ilean files which cannot be removed I think)
    • The directory structure must be intact so that the lean binary can detect Lean libraries; putting the contents of lib/ to /usr/lib/ may conflict with existing system libraries
  • Wrapper binary writes code to code.lean and runs lean --run code.lean
  • SVG logo is from the source code of lean-lang.org
  • include_str can include the source code as string. But interestingly, I can't find a way to abuse it to write a quine, as lean --run code.lean somehow rejects include_str "code.lean" or any other variation.

Todos:

  • Add codemirror-lean4-lsp as dependency and uncomment codemirror imports
  • Actually test if it works at all

Bubbler-4 and others added 10 commits August 12, 2026 16:57
@Bubbler-4
Add Lean Dockerfile
ae5631a
@Bubbler-4
Add lean.svg
ef98929 
Copied and slightly adjusted (viewBox and stroke color) from lean-lang.org source code
@Bubbler-4
Add Lean to latest-langs
ed523cf
@Bubbler-4
Add Lean to dev.Dockerfile
712dc94
@Bubbler-4
Add Lean to live.Dockerfile
447fbcb
@Bubbler-4
Add Lean to langs.toml
0a239ef
@Bubbler-4
Add Codemirror mode for Lean
cb3efac 
Commented out because `codemirror-lean4-lsp` should be added as dependency
@Bubbler-4
Add leanwrapper.c
e5f2bfc
@Bubbler-4
langs.toml: Fix location of Lean wrapper
a199cea
Bubbler-4
FIx various problems
a02ac1c 
- lean/Dockerfile: need to copy some .so files
- lean/leanwrapper.c: fix off by one error which chopped off first arg
- a-schema.sql: add lean as a possible lang key
JRaspass added a commit that referenced this pull request Aug 14, 2026
@JRaspass
Sort gigabyte-sized langs correctly
9e2ec15 
Updates #2714
Bubbler-4 and others added 3 commits August 16, 2026 14:33
Bubbler-4
Fix and improve wrapper
7a34d68 
- Avoid segfault from strcmp when argv[1] is null
- Compile and run in three steps to isolate warnings being printed to stdout, and move compilation warnings to stderr
@Bubbler-4
Merge branch 'code-golf:master' into add-lean
3e76110
Bubbler-4
Revert codemirror change for Lean
35e891b
@Bubbler-4

Bubbler-4 commented Aug 16, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Progress so far:

  • Lean runner can run submissions with or without arguments. I could solve Intersection, 12 Days of Christmas, and Emojify locally, and I checked that Ten-Pin Bowling's input comes into the program correctly.

  • By default, the compilation warnings are printed to stdout (IMO which should probably be fixed upstream). Instead of lean --run code.lean, the wrapper now has three steps:

    1. lean -c code.c code.lean (this part has stdout dup2'd to stderr)
    2. leanc -o code code.c
    3. code ...args

    code.lean and code.c are removed after code is produced, following what C++ wrapper does.

  • I tried to install codemirror-lean4-lsp. It didn't exist in npm, so I tried installing it from the github repo. It seemed to have configuration errors within the repo, so I couldn't try it.

Questions / Help wanted:

  • I don't see a way to show the logo properly. It's probably because the SVG is stroke-only unlike existing logos.
  • When I submit the same code multiple times, the first run takes much longer (>3000ms) than the rest (~300ms). Is it acceptable or should I fix it?

@Bubbler-4
Bubbler-4 marked this pull request as ready for review August 16, 2026 08:26
@Bubbler-4

Bubbler-4 commented Sep 11, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Note to future self: consider using https://leanprover.zulipchat.com/user_uploads/3121/_bE64eFQJ78Xlwhopqc_IH9A/Lean-stacked.svg as an alternative logo (source: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Square-friendly.20Lean.20logo.3F/near/585982317)

Lean stacked

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@Bubbler-4