lean4-ios

This repository contains:

1. A modified Lean 4 source tree so that the Lean runtime and stage0 standard library can be compiled with the iOS toolchain and linked into native iOS apps.

2. Lean Bindings for SDL3 / SDL3_ttf.

3. common Makefiles and C framework for building iOS SDL3 apps.

4. Some examples demonstrating how to use the framework.

Gallery

flappy flappy-example-video.MP4 Flappy Bird clone rendered with SDL.	lean-ios-runner On-device Lean elaborator / type-checker.
sdl-app sdl-example-video.MP4 SDL iOS app with animated 2D graphics.	bus-times Live TfL bus arrivals fetched over HTTP, rendered with SDL.
app Minimal Swift iOS app calling a Lean function via a C bridge.

Dependencies

1. Clone the repo including submodules (lean4, SDL, SDL_ttf, and resvg live as submodules under lean4/ and third-party/):

   git clone --recursive https://github.com/paulcadman/lean-ios.git
   

   Or, if you already cloned without --recursive:

   git submodule update --init --recursive
   

2. Install Xcode.

3. Install the Xcode command line tools:

   xcode-select --install
   

4. Install Homebrew, then install the build dependencies:

   brew install cmake zstd
   

5. Install Rust (the SDL-based examples link against resvg, which is built from source):

   curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
   

   Then add the iOS targets:

   rustup target add aarch64-apple-ios-sim aarch64-apple-ios
   

Building for physical device

Each example has a Makefile.device target that codesigns and installs the app on a connected iOS device. Invoke it with make -f Makefile.device run-device-app and set the following environment variables:

• DEVICE_ID — the device UDID or name (as shown by xcrun devicectl list devices).
• DEVICE_CODESIGN_IDENTITY — the codesigning identity to use (e.g. Apple Development: Your Name (TEAMID), as shown by security find-identity -v -p codesigning).
• DEVICE_PROVISION_PROFILE — path to a .mobileprovision file whose bundle identifier matches the example's APP_BUNDLE_ID (or SDL_APP_BUNDLE_ID).

Architecture

See docs/architecture.md for an overview of the project structure and build dependencies.