A running log of getting Lean 4 working on FreeBSD 14, kept as dated entries rather than rewritten in place: the body below is the original 4.23.0 / 14.3-RELEASE investigation, followed by addenda as the situation changed. Each addendum carries its own :VERIFIED_AT: so a later entry can correct an earlier one without either disappearing.

Formerly published at /research/lean4-4.23.0-freebsd-14.3/; that path now redirects here.

uname -srm

FreeBSD 14.3-RELEASE amd64

The FreeBSD lean4 package (version 4.23.0) fails to run with the error:

$ lean --version
error: failed to locate application

The lake build tool also fails with:

$ lake build
error: could not detect the configuration of the Lake installation

Using truss to trace system calls reveals the issue:

truss lean --version 2>&1 | grep -E "(readlink|error)"

Output:

readlink("/proc/80630/file",0x82076b5e0,1024) ERR#2 'No such file or directory'
error: failed to locate application

This script can be tangled and executed to set up Lean 4 on FreeBSD:

#!/bin/sh
# Lean 4 FreeBSD Setup Script
# Ensures procfs is mounted for Lean 4 to work

set -e

echo "=== Lean 4 FreeBSD Setup ==="
echo ""

# Check if running as root for fstab modification
check_root() {
    if [ "$(id -u)" -ne 0 ]; then
        echo "Note: Run with sudo for fstab modification"
        return 1
    fi
    return 0
}

# Add procfs to fstab if needed
setup_fstab() {
    if ! grep -q "^proc /proc procfs" /etc/fstab 2>/dev/null; then
        if check_root; then
            echo "Adding procfs to /etc/fstab..."
            echo 'proc /proc procfs rw 0 0' >> /etc/fstab
            echo "Done."
        else
            echo "Add this line to /etc/fstab:"
            echo "  proc /proc procfs rw 0 0"
        fi
    else
        echo "procfs already in /etc/fstab"
    fi
}

# Mount procfs if needed
mount_procfs() {
    if ! mount | grep -q "^procfs on /proc"; then
        if check_root; then
            echo "Mounting procfs..."
            mount /proc
            echo "Done."
        else
            echo "Run: sudo mount /proc"
        fi
    else
        echo "procfs already mounted"
    fi
}

# Verify Lean works
verify_lean() {
    echo ""
    echo "=== Verification ==="
    if command -v lean >/dev/null 2>&1; then
        echo "Lean version:"
        lean --version
        echo ""
        echo "Lake version:"
        lake --version
    else
        echo "Lean not found. Install with: pkg install lean4"
    fi
}

# Main
setup_fstab
mount_procfs
verify_lean

echo ""
echo "=== Setup Complete ==="

1. procfs is required: Lean 4 will not work without /proc mounted
2. This is not a packaging bug: The FreeBSD port is correctly built; the runtime dependency on procfs is undocumented
3. Persists across reboots: Adding to /etc/fstab ensures procfs is mounted at boot
4. elan not available: The elan version manager does not have FreeBSD binaries; use the pkg instead

• Veil DSL Workshop - Where this was discovered
• FreeBSD lean4 port
• Lean 4 Official Site
• POPL 2026 Veil Tutorial

echo "=== Full System Info ==="
echo "OS: $(uname -srm)"
echo "Lean: $(lean --version 2>&1)"
echo "Lake: $(lake --version 2>&1)"
echo "procfs: $(mount | grep 'procfs on /proc' || echo 'NOT MOUNTED')"
echo "pkg: $(pkg info lean4 2>&1 | grep Version || echo 'NOT INSTALLED')"

=== Full System Info ===
OS: FreeBSD 14.3-RELEASE amd64
Lean: Lean (version 4.23.0, x86_64-unknown-freebsd14.3, Release)
Lake: Lake version 5.0.0-src (Lean version 4.23.0)
procfs: procfs on /proc (procfs, local)
pkg: Version        : 4.23.0

On a second host (FreeBSD 14.4-RELEASE-p6, not the 14.3 box above), the fix in this note no longer applies directly: pkg search lean returns nothing Lean-related at all, so there is no lean4 package to install and mount procfs for. Both dead ends are real and this note's own "elan not available" line (Notes for Future Reference, item 4) still holds – but there's a third option that works instead of falling back to elan or giving up: if the host already runs FreeBSD's Linux compatibility layer (Linuxulator) for unrelated reasons, install the Linux build of elan and run it through that layer. A Linux-compiled elan correctly detects itself as Linux instead of hitting elan's missing-FreeBSD-platform panic, downloads Linux Lean binaries, and those binaries' own need for /proc/<pid>/file is already satisfied by linprocfs at /compat/linux/proc – the same underlying need this whole page is about, solved by infrastructure that was already there for other reasons.

kldstat -v | grep linux        # linux.ko loaded, linuxelf registered
pkg info | grep linux_base     # e.g. linux_base-rl9-9.7
mount | grep linprocfs         # linprocfs on /compat/linux/proc

12    1 0xffffffff830ee000    30b08 linux.ko (/boot/kernel/linux.ko)
                520 linuxelf
linux_base-rl9-9.7             Base set of packages needed in Linux mode (Rocky Linux 9.7)
linprocfs on /compat/linux/proc (linprocfs, local)

/compat/linux/bin/bash -c '
  export ELAN_HOME=$HOME/.elan-linux CARGO_HOME=$HOME/.elan-linux
  curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh
  /compat/linux/bin/bash /tmp/elan-init.sh -y --no-modify-path --default-toolchain none
'

A trap worth naming: a bare bash /tmp/elan-init.sh inside that outer /compat/linux/bin/bash -c '...' does not inherit the Linux personality – it resolves via $PATH like any other command, which still points at native FreeBSD bash unless every nested invocation pins the full /compat/linux/bin/bash path explicitly. Getting this wrong reproduces the exact failure this approach exists to avoid: the platform detection silently runs under real FreeBSD again and hits elan-x86_64-unknown-freebsd.tar.gz 404.

/compat/linux/bin/bash -c 'export PATH=$HOME/.elan-linux/bin:$PATH; lean --version; lake --version'

Lean (version 4.23.0, x86_64-unknown-linux-gnu, commit 50aaf682e9b74ab92880292a25c68baa1cc81c87, Release)
Lake version 5.0.0-src+50aaf68 (Lean version 4.23.0)

Verified past --version: a full downstream project's test suite (gmake verify in jwalsh/lean4-workshop – every example, exercise, solution and scratch file) passed completely this way, exit 0. Wrapped for reuse as bin/l4w-freebsd-linux in that repo, with the fuller writeup at docs/lean-on-freebsd.org.

This only helps when the target host already has the Linux compat layer set up for something else – standing one up from nothing is its own yak-shave, at which point GitHub Codespaces (as used for the 4.26.0/FreeBSD 15.0 case) is probably still less effort.

Same host as Addendum 1 (hydra, FreeBSD 14.4-RELEASE-p6 amd64). That addendum concluded pkg search lean "returns nothing Lean-related at all, so there is no lean4 package to install and mount procfs for", and proceeded to the Linux compat layer on that basis. The conclusion was sound given what the machine reported; the machine was reporting from a catalog that had not been updated in seven and a half months.

git -C /usr/ports log -1 --date=short --format='%h %ad'   # was: 2026-02-01
ls /var/db/pkg/repo-*.sqlite                               # was: no such file

The ports tree was pinned at 2026-02-01 and no binary catalogue had ever been fetched, so pkg search had nothing to search. After sudo git -C /usr/ports pull && sudo pkg update (tree to 2026-09-16, 37 837 + 38 238 packages catalogued), lean4 is present and installs normally.

pkg info lean4 | head -1
lean --version
make -C /usr/ports/math/lean4 -V DISTVERSION

Lean (version 4.29.0, x86_64-unknown-freebsd14.3, Release)
4.34.0

So on 14.4 the original fix on this page applies after all. The native port works, needing exactly what the body describes: procfs on /proc, added to /etc/fstab and mounted. The Linux compat route in Addendum 1 is still correct and still useful, but it is no longer the only option here, and it was never required for the reason given.

Worth separating: the freebsd14.3 in that version string is the build host baked into the target triple, not a mismatch with the 14.4 runtime.