Lean4Code

The Official Build Repo

Contact: adkisson@wustl.edu

What is this / why does this exist?

This repo contains the build files and official releases for Lean4Code, a VSCodium based Lean-native code editor. We wanted to minimize the bar of entry for getting started with Lean and using LeanDojo tools. This is our solution, a code editor with a truly intuitive Lean experience.

Supported versions:

Lean4Code is supported across all three major operating systems.
You can find the most recently compiled, prebuilt release of Lean4Code under the releases tab to the right of this page.

Built in features:

Lean4Code comes with…

• VSCode Lean4 extension downloaded and built in
• Automatic download and integration of LeanCopilot
• A one-click LeanDojo tracing experience
• An integrated agentic AI assistant

And we’re still working on new features!

Build instructions

1. Clone the repo

   git clone https://github.com/wadkisson/lean4code
   cd lean4code

2. Install npm in vscode dir / ⚠️WINDOWS USERS⚠️ - Extra setup is required here. Check the end of the README and come back to this part
   - From the main vscode directory (lean4code/vscode):

   npm install

Build commands for different systems

Once the extensions are properly build and compiled, run the appropriate build command from the vscode root dir (lean4code/vscode) to build the app!

macOS (Apple Silicon)

NODE_OPTIONS="--max-old-space-size=8192" npx gulp vscode-darwin-arm64

macOS (Intel)

NODE_OPTIONS="--max-old-space-size=8192" npx gulp vscode-darwin-x64

Linux (64-bit)

NODE_OPTIONS="--max-old-space-size=8192" npx gulp vscode-linux-x64

Windows (64-bit)

$env:NODE_OPTIONS="--max-old-space-size=8192"
npx gulp vscode-win32-x64

You can bump memory up to --max-old-space-size=16384 or more if needed.

---

And that’s it! We’ve designed the app to be as intuitive as possible. The Welcome Screen will guide you through how to use the built in LeanDojo tools.

⚠️Windows users⚠️

Building Lean4Code on Windows requires Visual Studio Build Tools for native dependencies. Follow these steps to download Visual Studio Build Tools and continue building Lean4Code.

1. Download Visual Studio Build Tools: https://visualstudio.microsoft.com/downloads/
2. Under the "Community" tab, click "Free Download"
3. Run the installer
4. In the installer:
   • Go to "Workloads", then check "Desktop development with C++"
   • Then go to the "Individual Components" tab, and then search for and enable "MSVC v143 - VS 2022 C++ x64/x86 Spectre-mitigated libs (Latest)"
5. Apply changes, wait for installation, then restart your computer. From here, you can continue with build instruction #2 as normal.

⚠️Mac Users⚠️

MacOS GateKeeper automatically puts a quarantine on all apps it doesn't recognize. To remove Lean4Code's quarantine, and start using the app, run this terminal command, where "path" refers to wherever you have Lean4Code stored: "xattr -rd com.apple.quarantine path/Lean4Code.app"