Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package metamath for openSUSE:Factory checked in at 2022-01-16 23:18:05 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/metamath (Old) and /work/SRC/openSUSE:Factory/.metamath.new.1892 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "metamath" Sun Jan 16 23:18:05 2022 rev:6 rq:946709 version:unknown Changes: -------- --- /work/SRC/openSUSE:Factory/metamath/metamath.changes 2021-03-24 16:11:32.691850401 +0100 +++ /work/SRC/openSUSE:Factory/.metamath.new.1892/metamath.changes 2022-01-16 23:19:05.770372499 +0100 @@ -1,0 +2,15 @@ +Sat Jan 15 20:44:21 UTC 2022 - Aaron Puchert <aaronpuch...@alice-dsl.net> + +- Update to version 0.198. + * Put two spaces between $c,v on same line in /rewrap. + * Fix cosmetic bug in WRITE SOURCE ... /REWRAP that prevented end + of sentence (e.g. period) from appearing in column 79, thus + causing some lines to be shorter than necessary. +- Use tarballs from GitHub because they have versioned URLs. +- Drop data package. There are no (recent) releases and the files + are just taken verbatim from https://github.com/metamath/set.mm + anyway. Users will likely want to work on these in their home + directory anyway, since they're not libraries. +- Only suggest the book to install. + +------------------------------------------------------------------- Old: ---- metamath.tar.bz2 metamath.tex New: ---- metamath-0.198.tar.gz metamath-book-20190602.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ metamath.spec ++++++ --- /var/tmp/diff_new_pack.IFrg3l/_old 2022-01-16 23:19:06.310372764 +0100 +++ /var/tmp/diff_new_pack.IFrg3l/_new 2022-01-16 23:19:06.314372766 +0100 @@ -1,8 +1,8 @@ # # spec file for package metamath # -# Copyright (c) 2021 SUSE LLC -# Copyright (c) 2021 Aaron Puchert +# Copyright (c) 2022 SUSE LLC +# Copyright (c) 2022 Aaron Puchert # # All modifications and additions to the file contributed by third parties # remain the property of their copyright owners, unless otherwise agreed @@ -25,20 +25,18 @@ %endif %define book_version 20190602 +%define book_tag second_edition # Global definitions Name: metamath -Version: 0.196 +Version: 0.198 Release: 0 Summary: Formal proof verifier and proof assistant License: GPL-2.0-or-later Group: Productivity/Scientific/Math URL: http://us.metamath.org/ -# Source links aren't stable. (They always points to the latest version.) -# http://us.metamath.org/downloads/metamath.tar.bz2 -Source0: %{name}.tar.bz2 -# http://us.metamath.org/latex/metamath.tex -Source1: %{name}.tex +Source0: https://github.com/metamath/metamath-exe/archive/refs/tags/v%{version}.tar.gz#/metamath-%{version}.tar.gz +Source1: https://github.com/metamath/metamath-book/archive/refs/tags/%{book_tag}.tar.gz#/metamath-book-%{book_version}.tar.gz BuildRequires: autoconf BuildRequires: automake BuildRequires: gcc @@ -54,9 +52,8 @@ BuildRequires: texlive-microtype BuildRequires: texlive-needspace BuildRequires: texlive-tabu -Recommends: %{name}-book = %{book_version} +Suggests: %{name}-book = %{book_version} %endif -Recommends: %{name}-data = %{version} BuildRoot: %{_tmppath}/%{name}-%{version}-build %description @@ -68,7 +65,7 @@ %package book Summary: The Metamath book License: CC0-1.0 -Group: Productivity/Scientific/Math +Group: Documentation/Other Version: %{book_version} Release: 0 Recommends: %{name} = %{VERSION} @@ -81,28 +78,8 @@ discussion of abstract mathematics and computers, with references to other proof verifiers and automated theorem provers. -%package data -Summary: Data base files for %{name} -License: CC0-1.0 AND GPL-2.0-or-later -Group: Productivity/Scientific/Math -Requires: %{name} = %{VERSION} -BuildArch: noarch - -%description data -This package contains Metamath data base files for several formal theories. -* set.mm ??? Logic and set theory database (see Ch. 3 of the Metamath book). -* nf.mm ??? Logic and set theory database for Quine's New Foundations set theory. -* hol.mm ??? Higher order logic (simple type theory) database. -* iset.mm ??? Intuitionistic logic database. -* ql.mm ??? Quantum logic database. -* demo0.mm ??? Demo of simple formal system (see Ch. 2 of the Metamath book). -* miu.mm ??? Hofstadter's MIU-system (see Appendix D of the Metamath book). -* big-unifier.mm ??? A unification stress test (see comments in the file). -* peano.mm ??? A presentation of Peano arithmetic by Robert Solovay. - %prep -%setup -q -n %{name} -rm metamath.exe +%setup -q -a 1 -n metamath-exe-%{VERSION}/ %build autoreconf -fi @@ -111,20 +88,18 @@ # Build documentation as outlined in the LaTeX file. %if %{with latex_doc} -touch metamath.ind -touch special-settings.sty -pdflatex %{SOURCE1} -pdflatex %{SOURCE1} -bibtex metamath -makeindex metamath.ind -pdflatex %{SOURCE1} -pdflatex %{SOURCE1} +pushd metamath-book-%{book_tag} +echo "Package amsmath Warning: Foreign command \\atop; +LaTeX Font Warning: Font shape \`TS1/cmtt/bx/n' undefined" >>allowed-errors +./generate-pdf +popd %endif %install %make_install %if %{with latex_doc} -install -Dm0644 metamath.pdf %{buildroot}%{_datadir}/%{name}/%{name}.pdf +install -Dm0644 metamath-book-%{book_tag}/metamath.pdf \ + %{buildroot}%{_datadir}/%{name}/%{name}.pdf %endif %files @@ -138,8 +113,4 @@ %{_datadir}/%{name}/%{name}.pdf %endif -%files data -%dir %{_datadir}/%{name} -%{_datadir}/%{name}/*.mm - %changelog
