wal.sh
home > research > lean4-4.23.0-freebsd-14 · Jan 01, 2026

Lean 4.23.0 on FreeBSD 14.3-RELEASE

lean4freebsdtheorem provertype theoryfunctional programminginstallationports

Lean 4.23.0 on FreeBSD 14.3-RELEASE

Table of Contents

1. Overview

This document records the steps required to get Lean 4.23.0 working on FreeBSD 14.3-RELEASE (amd64).

2. System Information

uname -srm

FreeBSD 14.3-RELEASE amd64

3. Problem Statement

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

4. Root Cause Analysis

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

4.1. The Problem

Lean 4 uses /proc/<pid>/file to determine its own executable path at runtime. This is a Linux-style procfs feature that FreeBSD supports, but only when procfs is mounted.

By default, FreeBSD does not mount procfs at /proc.

5. Solution

5.1. Step 1: Check current procfs status

mount | grep proc

linprocfs on /compat/linux/proc (linprocfs, local)
procfs on /proc (procfs, local)

5.2. Step 2: Add procfs to /etc/fstab (if not present)

# Check if procfs line exists in fstab
if ! grep -q "^proc /proc procfs" /etc/fstab; then
    echo "Adding procfs to /etc/fstab..."
    echo 'proc /proc procfs rw 0 0' | sudo tee -a /etc/fstab
else
    echo "procfs already in /etc/fstab"
fi

5.3. Step 3: Mount procfs (if not mounted)

# Mount procfs if not already mounted
if ! mount | grep -q "^procfs on /proc"; then
    echo "Mounting procfs..."
    sudo mount /proc
else
    echo "procfs already mounted"
fi

5.4. Step 4: Verify procfs is working

ls -la /proc/$$ | head -5

total 0
dr-xr-xr-x  1 jwalsh jwalsh 0 Jan  1 19:30 .
dr-xr-xr-x  1 root   wheel  0 Jan  1 19:04 ..
-r--r--r--  1 jwalsh jwalsh 0 Jan  1 19:30 cmdline
-rw-------  1 jwalsh jwalsh 0 Jan  1 19:30 dbregs

6. Validation

6.1. Lean Version

lean --version

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

6.2. Lake Version

lake --version

Lake version 5.0.0-src (Lean version 4.23.0)

6.3. Package Information

pkg info lean4 | grep -E "Name|Version|Flat size"

Name           : lean4
Version        : 4.23.0
Flat size      : 1.90GiB

7. Test Case: Building a Lean Project

7.1. Create a simple Lean file

-- Simple Lean 4 test
def hello := "Hello from Lean 4 on FreeBSD!"

#eval IO.println hello

-- Basic proof
theorem add_comm (a b : Nat) : a + b = b + a := Nat.add_comm a b

#check add_comm

7.2. Build and run

# Create test directory
mkdir -p /tmp/lean-test
cd /tmp/lean-test

# Create lakefile
cat > lakefile.lean << 'EOF'
import Lake
open Lake DSL

package «lean-test» where
  version := v!"0.1.0"

@[default_target]
lean_exe «test» where
  root := `test
EOF

# Create lean-toolchain
echo "leanprover/lean4:v4.23.0" > lean-toolchain

# Create test.lean
cat > test.lean << 'EOF'
def main : IO Unit := do
  IO.println "Hello from Lean 4 on FreeBSD!"
  IO.println s!"1 + 1 = {1 + 1}"
EOF

# Build
lake build 2>&1 | tail -3

# Run if build succeeded
if [ -f .lake/build/bin/test ]; then
  .lake/build/bin/test
fi

8. Complete Setup Script

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 ==="

9. Notes for Future Reference

  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

10. Related Links

11. Appendix: Full Diagnostic Commands

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