Name:           lean3
Version:        3.4.2
Release:        2%{?dist}
Summary:        A modern theorem prover and programming language

License:        ASL 2.0
URL:            https://leanprover.github.io/
Source0:        https://github.com/leanprover/lean/archive/v%{version}.tar.gz

BuildRequires:  cmake
BuildRequires:  gcc-g++
BuildRequires:  gmp-devel
BuildRequires:  make
Requires:       gmp
Requires:       libgcc
Requires:       libstdc++

%description
Theorem prover and a dependently typed purely functional programming language.

%prep
%setup -q -n lean-%{version}

%build
%cmake -DCMAKE_BUILD_TYPE=Debug ./src
%make_build

%install
%make_install

%check
ctest -V %{?_smp_mflags}

%files
%license LICENSE
%doc README.md
%doc doc/*.md
%{_bindir}/lean
%{_bindir}/leanchecker
%{_bindir}/leanpkg
%{_includedir}/lean.h
%{_includedir}/lean_*.h
%{_includedir}/lean_ext/*
%{_exec_prefix}/lib/lean/*
%{_exec_prefix}/lib/libleanshared.so
%{_exec_prefix}/lib/libleanstatic.a



%changelog
* Thu Aug 29 2019 Matěj Grabovský <mgrabovs@redhat.com> - 3.4.2-2
- Tweak list of required packages
- Add missing shared library to the list of bundled files

* Thu Aug 29 2019 Matěj Grabovský <mgrabovs@redhat.com> - 3.4.2-1
- Initial packaging of the latest and last 3.x version