Dmitry Roshchin
8f89ebddf9
Lean 4 programming language and theorem prover. Its build requires cadical: https://build.opensuse.org/requests/1237556 OBS-URL: https://build.opensuse.org/request/show/1237557 OBS-URL: https://build.opensuse.org/package/show/science/lean4?expand=0&rev=1
101 lines
3.2 KiB
RPMSpec
101 lines
3.2 KiB
RPMSpec
#
|
|
# 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
|