RFC: Native Linux riscv64 (RISC-V) support for the Lean 4 toolchain

RFC: Native Linux riscv64 (RISC-V) support for the Lean 4 toolchain

Summary

I’d like to propose adding (or completing) first-class support for running the Lean 4 toolchain natively on Linux riscv64. I’m willing to do the implementation work and open a pull request once maintainers agree on scope and approach.

This RFC focuses on native execution (building and running Lean 4 + core tooling on a riscv64 Linux machine), not bare-metal.

Motivation / user experience

RISC‑V Linux systems (servers, SBCs, research/education hardware) are becoming more common. Native support would:

• let users run lean/lake directly on riscv64 without emulation,
• improve portability and accessibility of Lean for new communities,
• reduce downstream patching / distro-specific workarounds.

Scope (what “support” means here)

In-scope

• Building Lean 4 from source on Linux riscv64 and running the resulting lean binary.
• Building and running lake (and compiling a small Lake project).
• Fixing architecture assumptions in build scripts / runtime where required.
• Adding at least a minimal CI signal to prevent regressions (details below).

Out-of-scope (at least initially)

• Non-Linux riscv64 targets.
• Bare-metal / embedded targets.
• Guaranteeing official prebuilt binaries (unless maintainers prefer this as part of acceptance).
• Any work that belongs in other repos (e.g. elan) unless maintainers explicitly want it included.

Proposed baseline environment

• Target: riscv64-unknown-linux-gnu (glibc)
• Toolchain: GCC or Clang as currently recommended by the project on Linux
• OS: a common riscv64 Linux distro (e.g. Debian/Ubuntu/Fedora riscv64), whichever maintainers prefer as the baseline.

Proposed approach

1. Build + smoke test on real riscv64

   • Ensure cmake/ninja (or whatever build is standard) completes successfully.
   • Smoke tests:
     • ./build/bin/lean --version
     • lake init hello && lake build
     • Run a small lean file (imports Init/Std).

2. Audit and fix platform/arch assumptions

   • Identify places that special-case architectures (x86_64/aarch64) and extend them to riscv64 where appropriate.
   • Fix any runtime / code generation / FFI / linker flag issues that show up on riscv64.

3. Testing / CI

   • Add a minimal CI job to keep riscv64 from regressing. Possible options (maintainer preference):
     • cross-build riscv64 artifacts (fast, but doesn’t run tests), or
     • run a limited smoke test suite under qemu-user/qemu-system, or
     • use native riscv64 runners if available.

4. Documentation

   • Document any riscv64-specific build notes (dependencies, flags, known limitations).

Why this belongs in lean4

Native riscv64 support is primarily about ensuring Lean’s core repo builds and runs correctly on that architecture, and about preventing regressions via tests/CI. Downstream-only patches tend to drift, and emulation-only is a poor UX.

Risks / considerations

• CI availability/performance (emulation can be slow).
• Subtle platform differences in the runtime or build system could require careful changes to avoid impacting other platforms.
• If “official binaries” are desired, coordination with release tooling may be needed.

Open questions for maintainers

1. What distro/toolchain should be the baseline for “Linux riscv64 supported”?
2. What level of CI is acceptable initially (cross-build only vs qemu smoke tests vs native runner)?
3. Should this RFC aim for “build-from-source works” first, or is “official release artifacts” required for considering support complete?
4. Are there known runtime/codegen constraints that would block riscv64?

Implementation willingness

If maintainers confirm the desired scope/acceptance criteria, I’m happy to:

• do the initial investigation,
• submit focused PRs (one issue per PR),
• add tests/CI where feasible,
• and stay responsive to review feedback.

Start by reviewing the proposed baseline environment and acceptance questions in the RFC. Build the toolchain on Linux riscv64, then run ./build/bin/lean --version, lake init hello && lake build, and the small Lean file described in the issue. Done requires an agreed scope, working native execution, and a maintainer-approved CI or smoke-test signal.