sorear's Metamath system engine - version 3 Rust
Rust
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
src
.gitignore
Cargo.lock
Cargo.toml
LICENSE-APACHE
LICENSE-MIT
README.md

README.md

SMM 3 - a Metamath database processor

A what?

Metamath is a language for expressing formal proofs, which makes few assumptions on the underlying logic and is simple enough to support a wide variety of tools. See http://us.metamath.org/#faq.

Building

Install Rust ([rustup.sh]), version 1.9.0 or later, then check out this repository and run:

cargo build --release

Alternatively using cargo install:

cargo install --git https://github.com/sorear/smetamath-rs
# $HOME/.cargo/bin/smetamath has been installed, use it as the binary in the following instructions

Running

# The largest known Metamath database, and best test case
git clone https://github.com/metamath/set.mm

# One-shot verification using 4 threads
target/release/smetamath --timing --jobs 4 --split --verify set.mm/set.mm

# Incremental verification
(while sleep 5; do echo; done) | target/release/smetamath --timing --jobs 4 --split --repeat --trace-recalc --verify set.mm/set.mm
# then make small changes to the beginning, end, or middle of the DB and observe how behavior changes

License

Licensed under either of

at your option.

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.