smetamath-rs
smetamath-rs copied to clipboard
sorear
sorear's Metamath system engine - version 3 Rust
Create a simple CI pipeline via GitHub actions. This does a basic "cargo test" on several different environments and two different versions of Rust. Eventually more checks can be added....
Remove unnecessary clone() calls; they take more time & removing them makes the code simpler. Signed-off-by: David A. Wheeler
Fix the Cargo.toml license entry ("/" is deprecated, since it's not part of the SPDX specification; use "OR" instead). This also updates the Cargo.lock file - lock files now include...
We should move all output to stderr (mostly error messages), except possibly timing info. This way, output-producing modes like `--export` can print their results on stdout without it getting confused...
There's a broad consensus that we want something sort of like a parsed representation of an MMJ2 worksheet. The details need to be worked out, probably in connection with smm-webui...
Currently, unlike the rest of the program `verify` will fail fast upon discovering any error in the proof at all. This makes sense because for the most part errors are...
A parsing algorithm for $j comments is needed to get basic grammar data, in particular, the identification of syntax proofs by typecode.
since we're now 7x faster than SMM2 _in single-threaded mode_, and using ~ a quarter the memory, it's probably still going to beat the JS version even with the overhead...