# Lean self-compiles a 180MB libleanshared + ~2400 .olean modules; debuginfo on the
# generated C is enormous and useless, and the bootstrap is sensitive to flag
# injection — keep the upstream release config and skip debuginfo extraction.
%global debug_package %{nil}

Name:           lean4
Version:        4.35.0
Release:        2%{?dist}
Summary:        Theorem prover and functional programming language (toolchain)

License:        Apache-2.0
URL:            https://lean-lang.org/
# Release archive includes stage0/ (a checked-in C-source snapshot of the
# compiler) so the bootstrap needs no pre-existing Lean or elan.
Source0:        https://github.com/leanprover/lean4/archive/refs/tags/v%{version}.tar.gz#/%{name}-%{version}.tar.gz

BuildRequires:  cmake
BuildRequires:  make
BuildRequires:  gcc
BuildRequires:  gcc-c++
BuildRequires:  clang
BuildRequires:  pkgconf-pkg-config
# 4.35's ExternalProject_Add(lean4lean/nanoda/con-leche/con-ron) needs a git executable
# at configure time even though those targets are EXCLUDE_FROM_ALL and never cloned.
BuildRequires:  git-core
# Lean 4.34 refuses to configure against GMP older than 6.3.0 (unsound corner cases).
BuildRequires:  gmp-devel >= 6.3.0
BuildRequires:  libuv-devel
BuildRequires:  openssl-devel
# find_program() picks these up so Lean does NOT download them at build time:
BuildRequires:  cadical
BuildRequires:  leangz

# Runtime: cadical is the SAT solver for decide/bv_decide; leantar (from leangz)
# is used by Lake to (un)pack library caches. We build with INSTALL_*=OFF so Lean
# ships no copies of its own — they come from these packages.
Requires:       cadical
Requires:       leangz
Requires:       clang
# leanc links executables with the full paths /usr/lib64/lib{gmp,ssl,crypto}.so, which
# only the -devel packages provide; without them `lake build` of any exe target fails.
Requires:       gmp-devel
Requires:       openssl-devel
# `lake check` (4.35) builds and exports the project inside a bubblewrap sandbox;
# without it only `lake check --inadvisably-no-sandbox` works.
Recommends:     bubblewrap

%description
Lean is an interactive theorem prover and a dependently-typed functional
programming language developed at the Lean FRO. This package provides the
Lean 4 toolchain: the `lean` compiler/checker, the `lake` build tool, the
`leanc` C-backend driver, and the bundled Init/Std/Lean libraries.

Note: this is the system toolchain. Projects that pin a specific toolchain via
`lean-toolchain` (the elan-managed workflow used by Mathlib) will not use it;
it is intended for building Lean code against the distribution toolchain.

%prep
%autosetup -n %{name}-%{version}

%build
# Root CMakeLists orchestrates stage0 (built from the checked-in C snapshot) then
# stage1; it forwards flags to both and does find_program(LEANTAR)/find_program(
# CADICAL) so the system tools are used (no network). USE_MIMALLOC=OFF drops the
# bundled-mimalloc FetchContent; INSTALL_{CADICAL,LEANTAR}=OFF avoids shipping
# copies that would file-conflict with the cadical and leangz packages.
# Raw cmake (not %%cmake): Lean's staged bootstrap is sensitive to injected flags,
# and stage0 deliberately discards extra CXX flags — match the validated invocation.
export CC=clang CXX=clang++
cmake \
    -S . -B build/release \
    -DCMAKE_C_COMPILER=clang \
    -DCMAKE_CXX_COMPILER=clang++ \
    -DSTAGE0_CMAKE_C_COMPILER=clang \
    -DSTAGE0_CMAKE_CXX_COMPILER=clang++ \
    -DCMAKE_BUILD_TYPE=Release \
    -DCMAKE_INSTALL_PREFIX=%{_prefix} \
    -DCMAKE_INSTALL_LIBDIR=lib \
    -DUSE_MIMALLOC=OFF \
    -DUSE_GMP=ON \
    -DUSE_GITHASH=OFF \
    -DLLVM=OFF \
    -DINSTALL_CADICAL=OFF \
    -DINSTALL_LEANTAR=OFF

# Lean's stdlib self-compile spikes multiple GB per process; cap parallelism by
# available RAM (>=3GB/job) so it never OOMs on a constrained builder.
cmake --build build/release %{limit_build -m 3000}

%install
# stage1 is an ExternalProject; install from its sub-build directory.
DESTDIR=%{buildroot} cmake --install build/release/stage1

# Lean installs its license files at the prefix root (/usr/LICENSE, /usr/LICENSES);
# drop them — the Apache-2.0 LICENSE is shipped properly via %%license below.
rm -f %{buildroot}%{_prefix}/LICENSE
rm -rf %{buildroot}%{_prefix}/LICENSES

%check
# Run the freshly installed toolchain out of the buildroot: its RUNPATH is
# $ORIGIN-relative and `lean` finds its sysroot from its own path.
export PATH=%{buildroot}%{_bindir}:$PATH
lean --version
lake --version
# Kernel replay of an installed module, then a file that needs the compiler's
# `decide` and the external SAT solver (cadical) behind `bv_decide`.
leanchecker -v Init.Prelude
cat > check.lean <<'EOF'
import Std.Tactic.BVDecide
theorem sum_range : (List.range 10).sum = 45 := by decide
theorem and_comm8 (x y : BitVec 8) : x &&& y = y &&& x := by bv_decide
def main : IO Unit := IO.println "lean4 ok"
EOF
lean check.lean

%files
%license LICENSE
%{_bindir}/lean
%{_bindir}/leanc
%{_bindir}/leanchecker
%{_bindir}/leanexport
%{_bindir}/leanir
%{_bindir}/leanmake
%{_bindir}/lake
%{_includedir}/lean/
%{_prefix}/lib/lean/
%{_prefix}/src/lean/
%{_datadir}/lean/

%changelog
* Fri Nov 06 2026 Morgan Hough <morgan.hough@gmail.com> - 4.35.0-2
- Rebuild in mhough/scientific: math and computational-physics packages move out
  of mhough/neurofedora

* Sat Oct 17 2026 Morgan Hough <morgan.hough@gmail.com> - 4.35.0-1
- Update to 4.35.0: adds `lake check` (re-verifies a project with leanchecker in a
  bubblewrap sandbox; Recommends: bubblewrap). Not built, by design: the extra
  kernels for `lake check --paranoid` (lean4lean, nanoda, con-leche, con-ron) and
  leanchecker-paranoid are fetched from git and need cargo, a network and
  USE_MIMALLOC=ON; they are EXCLUDE_FROM_ALL upstream.
- GMP >= 6.3.0 is now enforced by upstream's configure step (Fedora has 6.3.0).
- BuildRequires: git-core, for configure only (see the spec comment).
- Requires: gmp-devel, openssl-devel: leanc links exes against /usr/lib64/lib{gmp,ssl,crypto}.so
  (a clean chroot without them failed `lake build` of the demo exe; with them it builds).
- Ship the new /usr/bin/leanexport (the exporter `lake check` runs on the project).
- %check: lean/lake --version, leanchecker on Init.Prelude, and a file using
  `decide` and cadical-backed `bv_decide`.
- leantar pin in the root CMakeLists is still v0.1.20, which is our leangz.

* Sat Jun 20 2026 Morgan Hough <morgan.hough@gmail.com> - 4.31.0-1
- Initial package: Lean 4 theorem prover toolchain (lean, lake, leanc, leanchecker,
  leanir + bundled Init/Std/Lean libraries). Built from source via the stage0
  C-snapshot bootstrap (no elan). System gmp/libuv/cadical; leantar from leangz;
  USE_MIMALLOC=OFF and INSTALL_{CADICAL,LEANTAR}=OFF. Mathlib is out of scope
  (built per-project via Lake). $ORIGIN-relative RUNPATH (private /usr/lib/lean).