Skip to content
master
Go to file
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
doc
 
 
lib
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

README

This is smm (aka smetamath), a library to read and manipulate .mm files used by
the Metamath System (http://us.metamath.org/).  It is written in Javascript
(ES6 using Babel), and is known to work with io.js (recommended) 2.2.1 and
2.0.1, as well as node.js 0.8.28 and 0.10.38.  node.js 0.12.4 displays a
strange test failure, I'd avoid it for smm.  It is distributed under the MIT
license (LICENSE).

To install prerequisites and use smm to verify a set.mm file:

1. Install nvm from https://github.com/creationix/nvm (this will hack your
shell rcfile, and only works with Bourneish shells on Unix; if not Unix, skip
this step)

2. Install io.js 2+ and npm via "nvm install iojs" (Unix); (There is an
official io.js installer for Windows.  This worked with the pre-Babel version
and may still work.)

3. Download dependencies with "npm install" with the current directory as the
smm checkout.

4. Run self-tests: npm test

5. Make node-babel available: npm install -g babel

6. Use it: node-babel misc/verify.js ../set.mm

7. Ahead of time testing (somewhat faster, use this for benchmarks):

$$$ mkdir out
$$$ babel lib -d out/lib
lib/ABRStringStore.js -> out/lib/ABRStringStore.js
lib/ConsoleErrorFormatter.js -> out/lib/ConsoleErrorFormatter.js
lib/MMOM.js -> out/lib/MMOM.js
lib/NodeIO.js -> out/lib/NodeIO.js
lib/Parser.js -> out/lib/Parser.js
lib/Scoper.js -> out/lib/Scoper.js
lib/Verifier.js -> out/lib/Verifier.js
$$$ babel misc -d out/misc
misc/abr_stress.js -> out/misc/abr_stress.js
misc/gen_expon.js -> out/misc/gen_expon.js
misc/line_stress.js -> out/misc/line_stress.js
misc/repl.js -> out/misc/repl.js
misc/verify.js -> out/misc/verify.js
$$$ node out/misc/verify.js .../set.mm/set.mm
parse 778 ms
scope 232 ms
parser 667 ms
verify 4422 ms

About

sorear's Metamath system engine

Resources

License

Languages

You can’t perform that action at this time.