Test scripts

Test scripts may be run to test the system and to obtain working mdl math library from the original metamath library. To run tests first compile mdl, mm, smm and metamath with the command ‘./configure && make’. Then go to the directory ‘math’ and run appropriate script.

Translation tests


Script ‘translation’, runs a chain of translations and verification. <br>
To run the tests:

:~$./translation prop
:~$./translation math

Two new considerably big files (about 50 Mb each) will appear in this directory:

  • math.mdl : decompiled from math.mm theorem base in the mdl language,
  • math.smm : result of backwards translation of math.mm to the smm language,
    which is simplified metamath with an explicit policy of indexing via labeling and
    more rigid syntactic structure.

The last step of testing is verification of the resulting math.smm file with a corrected metamath program and a specific smm verifier.

Dir translation tests


Script ‘dir_translation’, does almost the same as a ‘translation’ test. In addition to translation and verification, it splits the original single file math library into a directory structure of mm, mdl and smm sources.
To run the tests:

:~$./dir_translation prop
:~$./dir_translation math

After script is run, following directories will appear: <br>

  • mm/: the original metamath base, which is split into the directory structure,
  • rus/: the mdl image of mm/,
  • smm/: the smm image of rus/.

Implicit steps prover test


Script ‘implicit_step_proving’ is used to show the ability of the prover to fill in the blank information of the implicit proof steps: which assertion may be used at this step and which steps/hypothesis may be used as a premises for this step.
To run the tests:

  • :~$./implicit_step_proving prop
  • :~$./implicit_step_proving math

Following files will automatically be created:

  • _implicit.mdl: decompiled from prop_small.mm with the step information removed,
  • _explicit.mdl: proved _implicit.mdl, the step information restored,
  • _explicit.smm: the smm image of _explicit.mdl.

At the end file _explicit.smm is verified both with metamath and smm programs.

CAUTION: complete test suite, which runs on the whole metamath theorem base, will demand about 1Gb of RAM.