#
# spec file for package lean4
#
# Copyright (c) 2025 Xu Zhao (i@xuzhao.net)
#
# All modifications and additions to the file contributed by third parties
# remain the property of their copyright owners, unless otherwise agreed
# upon. The license for this file, and modifications and additions to the
# file, is the same license as for the pristine package itself (unless the
# license for the pristine package is not an Open Source License, in which
# case the license is the MIT License). An "Open Source License" is a
# license that conforms to the Open Source Definition (Version 1.9)
# published by the Open Source Initiative.

# Please submit bugfixes or comments via https://bugs.opensuse.org/
#
%define         srcext             tar.zst
Name:           lean4
Version:        4.15.0
Release:        0
Summary:        Lean 4 programming language and theorem prover
License:        Apache-2.0
URL:            https://github.com/leanprover/lean4
Source:         lean4-%{version}.%{srcext}
Patch0:         prevent-copying-of-example-files.patch
Patch1:         fix-lib-install-dir.patch
Patch2:         fix-rpath.patch
BuildRequires:  ccache
BuildRequires:  cmake
BuildRequires:  cadical
BuildRequires:  chrpath
BuildRequires:  fdupes
BuildRequires:  gcc-c++
BuildRequires:  pkgconfig(gmp)
BuildRequires:  pkgconfig(libuv)
BuildRequires:  zstd


%description
Lean 4 programming language and theorem prover


%package devel
Summary:        Lean 4 development and header files

%description devel
Lean 4 development and header files

%prep
%autosetup -p1

%build
# Need to increase stack size
# https://github.com/leanprover/lean4/issues/6434
cmake -DINSTALL_LICENSE=OFF  -DCMAKE_BUILD_TYPE=RELEASE --preset release \
      -DINCLUDE_INSTALL_DIR:PATH=/usr/include \
      -DLIB_INSTALL_DIR:PATH=/usr/lib64
make -C build/release %{?_smp_mflags}

%install
cd build/release/stage1
# install bin files
install -Dm755 bin/lake %{buildroot}%{_bindir}/lake
install -Dm755 bin/lean %{buildroot}%{_bindir}/lean
install -Dm755 bin/leanc %{buildroot}%{_bindir}/leanc
install -Dm755 bin/leanmake %{buildroot}%{_bindir}/leanmake
strip --strip-debug --strip-unneeded %{buildroot}%{_bindir}/lake
strip --strip-debug --strip-unneeded %{buildroot}%{_bindir}/lean
strip --strip-debug --strip-unneeded %{buildroot}%{_bindir}/leanc
# install library files
chrpath -d lib/lean/*.so
install -Dm644 lib/lean/libInit_shared.so %{buildroot}%{_libdir}/lean/libInit_shared.so
install -Dm644 lib/lean/libLake_shared.so %{buildroot}%{_libdir}/lean/libLake_shared.so
install -Dm644 lib/lean/libleanshared.so %{buildroot}%{_libdir}/lean/libleanshared.so
install -Dm644 lib/lean/libleanshared_1.so %{buildroot}%{_libdir}/lean/libleanshared_1.so
strip --strip-debug --strip-unneeded %{buildroot}%{_libdir}/lean/*.so

cp -r include %{buildroot}%{_includedir}
rm %{buildroot}%{_includedir}/lean/lean_libuv.h
cp -r share %{buildroot}%{_datadir}
# replace shebang
sed -i "s|#!/usr/bin/env bash|#!/bin/bash|g" %{buildroot}%{_bindir}/leanmake

%fdupes %{buildroot}

%files devel
%{_includedir}/lean

%files
%license LICENSE
%doc README.md RELEASES.md
%{_bindir}/lake
%{_libdir}/lean
%{_bindir}/lean
%{_bindir}/leanc
%{_bindir}/leanmake
%{_datadir}/lean


%changelog