| Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
| Name: metamath | Distribution: openSUSE:Factory:zSystems |
| Version: 0.198 | Vendor: openSUSE |
| Release: 7.10 | Build date: Sat Apr 30 14:04:31 2022 |
| Group: Productivity/Scientific/Math | Build host: reproducible |
| Size: 887195 | Source RPM: metamath-0.198-7.10.src.rpm |
| Packager: https://bugs.opensuse.org | |
| Url: http://us.metamath.org/ | |
| Summary: Formal proof verifier and proof assistant | |
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.
GPL-2.0-or-later
* Sat Apr 30 2022 Aaron Puchert <[email protected]>
- Disable build of metamath-book on Tumbleweed: it doesn't build
with TeXlive 2022 because of what seems to be a bug in
texlive-tabu. (gh#metamath/metamath-book#235)
- Use symbolic dependencies for required TeX packages.
* Sat Jan 15 2022 Aaron Puchert <[email protected]>
- 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.
* Wed Mar 03 2021 Aaron Puchert <[email protected]>
- Update to version 0.196.
* Fix bug causing new axioms to be used by MINIMIZE_WITH.
* Add "Claim" to bib ref types.
* Remove error check for $e <- $f assignments.
* Check for discouragement tags in *ALT, *OLD labels in
VERIFY MARKUP.
* Add underscore checking in VERIFY MARKUP and add /UNDERSCORE-
_SKIP qualifier; also check for trailing space on lines.
* Refine prevention of WRITE SOURCE.../REWRAP from modifying
comments containing "<HTML>".
* Allow space in TOOLS> BREAK.
* Add checking for mathbox independence to VERIFY MARKUP;
add /MATHBOX_SKIP.
* "PROVE =" will now resume the previous MM-PA session if there
was one; allow "~" to start/end with blank (meaning first/last
statement); add "@1234".
* Add /INCLUDE_MATHBOXES to to IMPROVE; notify user upon ASSIGN
from another mathbox.
* Print message when IMPROVE or MINIMIZE_WITH uses another mathbox.
* Add CONJECTURE, RESULT to [bib] keywords.
* Add HELP BIBLIOGRAPHY.
* Added CONCLUSION FACT INTRODUCTION PARAGRAPH SCOLIA SCOLION
SUBSECTION TABLE to [bib] keywords.
* Added WRITE SOURCE ... /EXTRACT ....
* Make the output of /EXTRACT stable in the sense that, with the
same <label-list> parameter, extract(extract(file)) =
extract(file) except that the date stamp at the top will be
updated. (The first extraction even if "*" will usually be
different because it discards non-relevant content. Note that
the include file directives "$( $[ Begin..." etc. and comments
with "$j" are currently discarded.)
* Add keyword "htmlexturl" to $t statement in .mm file.
* Prevent "htmlexturl" links from wrapping.
* Temporarily disable /REWRAP until bug fixed.
* Fix bug that deleted comments that were followed by ${, $}, $c,
$v, $d on the same line.
- Relax dependencies.
* Fri Dec 20 2019 Aaron Puchert <[email protected]>
- Update to version 0.180.
* MINIMIZE_WITH axiom trace now starts from current NEW_PROOF
instead of SAVEd proof.
* Make sure traceback flags are cleared after MINIMIZE_WITH.
* Add url pointer to HELP WRITE SOURCE /SPLIT.
* Clarify HELP WRITE SOURCE /REWRAP.
* Add bug check info for user.
* Use '|->' (not 'e.') as syntax hint for maps-to.
* Remove extraneous </TD>.
* Fix "line 0" in error msg when label clashes with math symbol.
* Improve TOOLS> HELP INSERT, DELETE.
* Change bug 1511 to error message.
* Trigger Most Recent link on mmtheorems.html when there is a
mathbox statement (currently set.mm and iset.mm).
* Improve help for TOOLS> DELETE and SUBSTITUTE.
* Change "htmlHome" in warnings to "htmlhome".
* Wed Sep 25 2019 Aaron Puchert <[email protected]>
- Update to version 0.178.
- Update book to version 20190602.
- Remove Windows executable from sources before building.
* Wed May 01 2019 [email protected]
- Update to version 0.177.
- Update book to version 20190407.
- Use man page from upstream now.
* Thu Apr 04 2019 [email protected]
- Change SPDX identifier to GPL-2.0-or-later, as README.TXT states.
* Tue Mar 19 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 2019 [email protected]
- Fix version number.
* Sat Mar 16 2019 Jan Engelhardt <[email protected]>
- Remove %if..%endif guards that do not change the build result.
- Itemize the list in the description.
/usr/bin/metamath /usr/share/licenses/metamath /usr/share/licenses/metamath/LICENSE.TXT /usr/share/man/man1/metamath.1.gz
Generated by rpm2html 1.8.1
Fabrice Bellet, Wed Dec 4 00:10:59 2024