Gramm is an Antlr4-based Metamath proof verifier. From the supplied Metamath grammar (MM.g4), Antlr4 creates a lexer/parser pair and provides support code for walking the generated parse trees. Here's a small branch from set.mm's tree:
We walk the tree by extending an Antlr4-provided empty base listener. At
particular terminal nodes of the tree, tokens are gathered and sent to the
global scope manager for processing. The most important processing occurs via
proof nodes and involves calls to the proof verifier. A bit more detail
can be found here.
After cloning the project, navigate to its root and run:
$ mvn package
gramm-x.y.z.jar will be created in the
(you can ignore the second created jar,
original-gramm-x.y.z.jar). If you
prefer to run tests prior to building the jar, run:
$ mvn package -DskipTests=false
Then again, you can skip the cloning/building and just download the pre-built executable.
Note: in place of
set.mm, you can substitute any Metamath database.
$ java -jar -Xmx1g gramm-0.1.7.jar set.mm reading source file set.mm ... verifying source file set.mm ... 0 errors 0 warnings 31705 of 31705 proofs were verified time: 9.73 sec
Gramm is distributed under the MIT License.
Although Gramm does not bundle any third party libraries, it depends on the Antlr4 runtime, and the executable jar will contain Antlr class files. Antlr4 is distributed under the BSD 3-Clause License.
The Metamath files in the
test/resourcesdirectory are in the public domain or available under the CC0 1.0 Universal License, with the exception of
peano-fixed.mm, which is distributed under the GPL License. See each file for full details. Many of these files were copied from David Wheeler's github project: https://github.com/david-a-wheeler/metamath-test.