Hello community, here is the log from the commit of package metamath for openSUSE:Factory checked in at 2019-06-19 20:54:53 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/metamath (Old) and /work/SRC/openSUSE:Factory/.metamath.new.4811 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "metamath" Wed Jun 19 20:54:53 2019 rev:1 rq:691613 version:unknown Changes: -------- New Changes file: --- /dev/null 2019-06-06 01:32:53.891093091 +0200 +++ /work/SRC/openSUSE:Factory/.metamath.new.4811/metamath.changes 2019-06-19 20:54:56.693802747 +0200 @@ -0,0 +1,88 @@ +------------------------------------------------------------------- +Thu Apr 4 20:55:37 UTC 2019 - [email protected] + +- Change SPDX identifier to GPL-2.0-or-later, as README.TXT states. + +------------------------------------------------------------------- +Tue Mar 19 23:32:32 UTC 2019 - [email protected] + +- Fix dependency versions - since the book has a different version, + we need to be careful which version we refer to. + +------------------------------------------------------------------- +Sat Mar 16 18:08:59 UTC 2019 - [email protected] + +- Fix version number. + +------------------------------------------------------------------- +Sat Mar 16 17:03:35 UTC 2019 - Jan Engelhardt <[email protected]> + +- Remove %if..%endif guards that do not change the build result. +- Itemize the list in the description. + +------------------------------------------------------------------- +Sat Mar 16 14:37:53 UTC 2019 - [email protected] + +- Update to version 0.175. +- Update Metamath book to version 20190307. +- Use date as version number for Metamath book, because it isn't + versioned alongside the program. +- Move source links into comments, as they aren't stable. They + always point to the latest version, which isn't compatible with + download_files service runs. + +------------------------------------------------------------------- +Thu Mar 7 20:45:21 UTC 2019 - [email protected] + +- Update to version 0.174. +- Package Metamath book separately. + +------------------------------------------------------------------- +Tue Jan 8 23:48:34 UTC 2019 - [email protected] + +- Update to version 0.171. + +------------------------------------------------------------------- +Mon Aug 6 21:18:20 UTC 2018 - [email protected] + +- Update to version 0.163. +- Recommend data package, make it noarch. + +------------------------------------------------------------------- +Sun Feb 4 22:58:39 UTC 2018 - [email protected] + +- Add a brief manual page. +- Do not build LaTeX docs on SLES, because TeXlive doesn't seem up + to the task there. + +------------------------------------------------------------------- +Sun Feb 4 19:20:30 UTC 2018 - [email protected] + +- Update to version 0.161. +- Also build documentation. +- Package data base files separately. + +------------------------------------------------------------------- +Tue Oct 24 20:35:00 UTC 2017 - [email protected] + +- Update version to 0.155. + +------------------------------------------------------------------- +Wed Jul 19 14:00:00 UTC 2017 - [email protected] + +- Really update version to 0.146. + +------------------------------------------------------------------- +Wed Jul 19 13:55:00 UTC 2017 - [email protected] + +- Update version to 0.146. + +------------------------------------------------------------------- +Sat Apr 15 11:45:00 UTC 2017 - [email protected] + +- Update version to 0.139. + +------------------------------------------------------------------- +Mon Oct 31 23:27:00 UTC 2016 - [email protected] + +- Initial release of the package base on version 0.130. New: ---- metamath.1 metamath.changes metamath.spec metamath.tar.bz2 metamath.tex ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ metamath.spec ++++++ # Specification for package metamath # # Copyright (c) 2016-2019 by Aaron Puchert # # 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. # Do not build LaTeX docs on SLES. %if 0%{?is_opensuse} %bcond_without latex_doc %else %bcond_with latex_doc %endif %define book_version 20190307 # Global definitions Name: metamath Version: 0.175 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 Source2: %{name}.1 BuildRequires: autoconf BuildRequires: automake BuildRequires: gcc %if %{with latex_doc} BuildRequires: texlive-amsfonts BuildRequires: texlive-anysize BuildRequires: texlive-bibtex-bin BuildRequires: texlive-breqn BuildRequires: texlive-hyperref BuildRequires: texlive-latex-bin BuildRequires: texlive-makecell BuildRequires: texlive-makeindex-bin BuildRequires: texlive-microtype BuildRequires: texlive-needspace BuildRequires: texlive-tabu Recommends: %{name}-book = %{book_version}-%{release} %endif Recommends: %{name}-data = %{version}-%{release} BuildRoot: %{_tmppath}/%{name}-%{version}-build %description The Metamath language is a language to write theorems and formal proofs for them. The Metamath program can parse files in the Metamath language and verify the proofs. You can find examples of theories developed in Metamath on the website. %package book Summary: The Metamath book Version: %{book_version} License: CC0-1.0 Group: Productivity/Scientific/Math Requires: %{name} = %{VERSION}-%{release} BuildArch: noarch %description book The Metamath book, written by Norman Megill with extensive revisions by David A. Wheeler, 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. %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}-%{release} 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} %build autoreconf -fi %configure make %{?_smp_mflags} # 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 pdflatex %{SOURCE1} pdflatex %{SOURCE1} %endif %install %make_install install -Dm0644 %{SOURCE2} %{buildroot}%{_mandir}/man1/%{name}.1 %if %{with latex_doc} install -Dm0644 metamath.pdf %{buildroot}%{_datadir}/%{name}/%{name}.pdf %endif %files %license LICENSE.TXT %{_bindir}/%{name} %{_mandir}/man1/%{name}.1%{ext_man} %if %{with latex_doc} %files book %dir %{_datadir}/%{name} %{_datadir}/%{name}/%{name}.pdf %endif %files data %dir %{_datadir}/%{name} %{_datadir}/%{name}/*.mm %changelog ++++++ metamath.1 ++++++ .\" t -*- coding: UTF-8 -*- .\" Man page for metamath .\" .\" Copyright (C) 2018 Aaron Puchert. .\" .\" You may distribute under the terms of the GNU General Public .\" License as specified in the file COPYING that comes with the .\" man-db distribution. .\" .TH metamath 1 "2018-02-04" Metamath "User Manuals" .SH NAME metamath \- Formal proof verifier and proof assistant .SH SYNOPSIS .BI "metamath [ " "commands" " | " "file" " ]" .SH DESCRIPTION .B metamath is a formal proof verifier and proof assistant for the Metamath language. It can be initialized via a series of .I commands or with a data base .IR file , which can then be explored interactively. .PP For details about the Metamath language and the command-line interface, type .B help into the command prompt, or read the Metamath book [1], which should have been installed along with the package. .SH LANGUAGE A Metamath database consists of a sequence of three kinds of tokens separated by white space (which is any sequence of one or more white space characters). The set of keyword tokens is .BR ${ ", " $} ", " $c ", " $v ", " $f ", " $e ", " $d ", " $a ", " $p ", " .BR $. ", " $= ", " $( ", " $) ", " $[ ", and " $] . The last four are called auxiliary or preprocessing keywords. A .I label token consists of any combination of letters, digits, and the characters hyphen, underscore, and period. The label of an assertion is used to refer to it in a proof. A math .I symbol token may consist of any combination of the 93 printable .BR ascii (7) characters other than .BR $ . All tokens are case-sensitive. .TP .BI $( " comment " $) Comments are ignored. .TP .BI $[ " file " $] Include the contents of a .IR file . .TP .BI ${ " statements " $} Scoped block of statements. A math symbol becomes active when declared and stays active until the end of the block in which it is declared. .TP .BI $v " symbols " $. Declare .I symbols as variables. A variable may not be declared a second time while it is active, but it may be declared again (as a variable, but not as a constant) after it becomes inactive. .TP .BI $c " symbols " $. Declare .I symbols as constants. A constant must be declared in the outermost block and may not be declared a second time. .TP .IB "label " $f " constant variable " $. Variable-type hypothesis to specify the nature or type of a variable (such as `let x be an integer.'). A variable must have its type specified in a .B $f statement before it may be used in a .BR $e ", " $a ", or " $p statement. There may not be two active .B $f statements containing the same variable. .TP .IB "label " $e " constant symbols " $. Logical hypothesis, expressing a logical truth (such as `assume x is prime') that must be established in order for an assertion requiring it to also be true. .TP .BI $d " variables " $. Disjoint variable restriction. For distinct active .IR variables , it forbids the substitution of one variable with another. .TP .IB "label " $a " constant symbols " $. Axiomatic assertion. .TP .IB "label " $p " constant symbols " $= " proof " $. Provable assertion. The .I proof is a sequence of statement .IR label s. This label sequence serves as a set of instructions that the Metamath program uses to construct a series of math symbol sequences. The construction must ultimately result in the math symbol sequence contained between the .BR $p " and " $= keywords of the .B $p statement. For details, see section 4.3 in [1]. Proofs are most easily written using the interactive prompt in .BR metamath . .SH FILES .I /usr/share/metamath .RS Data base files for several formal theories. .SH SEE ALSO .B "[1]" Norman Megill: .UR http://us.metamath.org/downloads/metamath.pdf Metamath, A Computer Language for Pure Mathematics .UE . ++++++ metamath.tex ++++++ ++++ 15177 lines (skipped)
