Name:           lean-repl
Version:        4.31.0
Release:        1%{?dist}
Summary:        JSON read-eval-print interface to the Lean 4 theorem prover

License:        Apache-2.0
URL:            https://github.com/leanprover-community/repl
Source0:        %{url}/archive/refs/tags/v%{version}/repl-%{version}.tar.gz

# lean4 ships the lake/lean/leanc build toolchain. The REPL is compiled against
# a specific Lean version (this tag pins leanprover/lean4:v%{version}), so the
# build- and runtime-requires are pinned to the matching lean4. (lean4 lives in
# this COPR, not Fedora.)
BuildRequires:  lean4 = %{version}
# Lean transpiles to C and invokes the C compiler (via leanc) to build/link
# against the Lean runtime's libraries (libstdc++, gmp, libuv).
BuildRequires:  gcc
BuildRequires:  gcc-c++
BuildRequires:  gmp-devel
BuildRequires:  libuv-devel
Requires:       lean4%{?_isa} = %{version}

# Lean emits its own optimized native code via leanc; skip rpm debuginfo.
%global debug_package %{nil}

%description
REPL provides a read-eval-print loop and a JSON-based command interface to the
Lean 4 theorem prover: send commands, tactics and proof terms and receive the
resulting proof state, messages and errors as structured JSON. It is the
substrate that many AI and automation tools (for example LeanDojo) use to drive
Lean programmatically. The interface binary is installed as %{_bindir}/lean-repl.

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

%build
# Build against the system Lean toolchain (no elan); REPL has no Lake deps.
lake build repl

%install
install -Dpm0755 .lake/build/bin/repl %{buildroot}%{_bindir}/lean-repl

%files
%license LICENSE
%doc README.md
%{_bindir}/lean-repl

%changelog
* Wed Jun 24 2026 Morgan Hough <morgan.hough@gmail.com> - 4.31.0-1
- Initial package: Lean 4 REPL / JSON interface (binary installed as lean-repl)