Name:           metamath
Version:        0.139
Release:        1%{?dist}
Summary:        Construct mathematics from basic axioms

License:        GPLv2+
URL:            http://us.metamath.org/
Source0:        http://us.metamath.org/downloads/%{name}.tar.bz2
Source1:        http://us.metamath.org/latex/%{name}.tex

BuildRequires:  automake
BuildRequires:  gcc
BuildRequires:  tex(latex)

Suggests:       rlwrap

%description
Metamath is a tiny language that can express theorems in abstract
mathematics, accompanied by proofs that can be verified by a computer
program.  Metamath lets you see mathematics developed in complete detail
from first principles, with absolute rigor.

%package        theories
Summary:        Existing mathematical theories in the metamath format
Requires:       %{name} = %{version}-%{release}
BuildArch:      noarch

# peano.mm is GPLv2+; all other theory files are CC0
License:        GPLv2+ and CC0

%description    theories
This package contains metamath theory files for several branches of
mathematics, such as ZFC set theory, HOL, and Peano arithmetic.

%package        doc
Summary:        The Metamath book
License:        CC0
BuildArch:      noarch

%description    doc
This package contains The Metamath book, which provides an in-depth
understanding of the Metamath language and program.  The first part of
the book also includes an easy-to-read informal discussion of abstract
mathematics and computers, with references to other proof verifiers and
automated theorem provers.

%prep
%setup -q -n %{name}
cp -p %{SOURCE1} .

# Remove prebuilt objects
rm metamath.exe

# Do not override our choice of CFLAGS
sed -i '/Try to optimize/,/^$/d' configure.ac

# Generate the configure script
autoreconf -fi

%build
%configure CFLAGS="%{optflags} -fwrapv"
make %{?_smp_mflags}

# Build the manual
touch metamath.ind
pdflatex metamath
pdflatex metamath
bibtex metamath
makeindex metamath.idx
pdflatex metamath
pdflatex metamath
pdflatex metamath

%install
%make_install

# Install all of the theories
cp -p *.mm %{buildroot}%{_datadir}/metamath

# Install the manual
mkdir -p %{buildroot}%{_docdir}/%{name}
cp -p %{name}.pdf %{buildroot}%{_docdir}/%{name}

%files
%doc README.TXT
%license LICENSE.TXT
%{_bindir}/metamath

%files theories
%{_datadir}/metamath/

%files doc
%license LICENSE.TXT
%dir %{_docdir}/metamath/
%{_docdir}/metamath/metamath.pdf

%changelog
* Tue Feb 14 2017 Jerry James <loganjerry@gmail.com> - 0.139-1
- New upstream version (bz 1406763)
- Install all of the theories (bz 1422091)

* Fri Feb 10 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.138-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild

* Thu Dec 29 2016 Jerry James <loganjerry@gmail.com> - 0.138-1
- New upstream version (bz 1406763)

* Mon Sep 19 2016 Jerry James <loganjerry@gmail.com> - 0.135-1
- New upstream version (bz 1377308)

* Sat Aug 27 2016 Jerry James <loganjerry@gmail.com> - 0.134-1
- New upstream version (bz 1370745)

* Fri Aug 19 2016 Jerry James <loganjerry@gmail.com> - 0.133-1
- New upstream version

* Mon Jul 18 2016 Jerry James <loganjerry@gmail.com> - 0.132-1
- New upstream version

* Tue Jun 21 2016 Jerry James <loganjerry@gmail.com> - 0.131-1
- New upstream version

* Wed May 11 2016 Jerry James <loganjerry@gmail.com> - 0.125-2
- Fix unowned directory
- Add the manual

* Fri May  6 2016 Jerry James <loganjerry@gmail.com> - 0.125-1
- Initial RPM