RunningTheMMJ2TestSuite

Running The mmj2 Test Suite

Factoids:

The mmj2.zip download file contains a number of tests that exercise the mmj2 logic and are used to validate each software release.
The tests are intended to be run as "parallel tests". That is, the same test is executed with new and old software versions and the output from the tests is compared using file comparison software.
All of the tests invoke the executable code: C:\mmj2\mmj2jar\mmj2.jar. An easy way to run the tests using two versions of the software is to backup mmj2.jar to say, "mmj2old.jar" and create a "mmj2new.jar" -- then, prior to running the tests, update/overlay the "mmj2.jar" file with the jar file from the desired software version (this is crude but effective :)
Some of the tests use an archived version of Metamath's set.mm file as input (mmj2\data\mm\RegressionTest1set.mm), while others use hand-crafted .mm files as input.
In some of the tests, the intent is to create a severe error condition that causes mmj2 to immediately terminate processing, and the termination output is saved for comparison. Therefore, it is recommended that the tests be run using a software package or shell that can capture System.err output lines (for example the "TextPad" software program, which also has a rudimentary file comparison utility.)
The final test output prior to release of a new mmj2 software version is stored in directory c:\mmj2\data\result. Each test generates an "Err" -- System.err -- output file, as well as an "Out" -- System.out -- output file. These are provided for informational purposes, but unless the version of set.mm that was used to generate the test output is available, it is necessary to rerun the tests using the latest version of set.mm using the old software.
The letters "UT" in the output file names stand for Unit Test.
The letters "VT" in the output file names stand for Volume Test.

Instructions:

The following (left-hand column) .bat files are located in c:\mmj2\test\windows

RunSample001.bat	Update `C:\mmj2\test\windows\RunSample001.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Update `c:\mmj2\data\runparm\windows\Sample001.txt` RunParm `SystemOutputFile` file name with the correct data and suffix ("`20061002a`" = old software, "`20061002b`" = new software). If the file is new, specify option "`new`", otherwise specify "`update`". Run `c:\mmj2\test\windows\Sample001.bat`. There should be no error file to save -- and the Command Window output is not significant. Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed. NOTE: Look at "`LogSysCounts: stmtTbl.size()=`" in the output file, "`C:\mmj2\data\result\Sample001Sysout`YYYYMMDD`d.txt`", as well as "`symTbl.size()`". The default initial table sizes for your .mm should be approximately 1.5 times `stmtTbl.size()` and `symTbl.size()` (if too small there will be a wasteful automatic resizing of the internal HashMaps). To update the default initial sizes you can change the source code at mmj.lang.LangConstants.java : `SYM_TBL_INITIAL_SIZE_DEFAULT` and `STMT_TBL_INITIAL_SIZE_DEFAULT`. Alternatively, you can input these RunParms to override the defaults at runtime: `SymbolTableInitialSize` and `StatementTableInitialSize`.
RunSample002.bat	Update `C:\mmj2\test\windows\RunSample002.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Update `c:\mmj2\data\runparm\windows\Sample002.txt` RunParm `SystemOutputFile` AND `SystemErrorFile` file names with the correct data and suffix ("`20061002a`" = old software, "`20061002b`" = new software). This example shows how to use "`new`" and "`update`". Run `c:\mmj2\test\windows\RunSample002.bat`. The Command Window output is not significant (should be just a log of processing with no errors.) Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed.
RunSample003.bat	Update `C:\mmj2\test\windows\RunSample003.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Update `c:\mmj2\data\runparm\windows\Sample003.txt` RunParm `SystemOutputFile` file name with the correct data and suffix ("`20061002a`" = old software, "`20061002b`" = new software). If the file is new, specify option "`new`", otherwise specify "`update`". Run `c:\mmj2\test\windows\RunSample003.bat`. There should be no error file to save -- and the Command Window output is not significant. Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed.
RunUnitTest1.bat	Update `C:\mmj2\test\windows\RunUnitTest1.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunUnitTest1.bat`. Manually save the Command Window output to `C:\mmj2\data\result\UT1Err20061002a.txt` (using the date and suffix chosen for the test.) Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed.
RunUnitTest2.bat	Update `C:\mmj2\test\windows\RunUnitTest2.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunUnitTest2.bat`. Note: don't bother manually saving the Command Window output -- it is not significant for UnitTest2. Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed.
RunUnitTest3.bat	Update `C:\mmj2\test\windows\RunUnitTest3.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunUnitTest3.bat`. Manually save the Command Window output to `C:\mmj2\data\result\UT3Err20061002a.txt` (using the date and suffix chosen for the test.) Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed.
RunUnitTest4.bat	Update `C:\mmj2\test\windows\RunUnitTest4.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunUnitTest4.bat`. Note: don't bother manually saving the Command Window output -- it is not significant for UnitTest4. Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed.
RunUnitTest5.bat	Update `C:\mmj2\test\windows\RunUnitTest5.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunUnitTest5.bat`. Note: don't bother manually saving the Command Window output -- it is not significant for UnitTest5. Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed.
`RunUnitTest6.bat`	Update `C:\mmj2\test\windows\RunUnitTest6.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunUnitTest6.bat`. Note: don't bother manually saving the Command Window output -- it is not significant for UnitTest6. Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed.
`RunUnitTest7.bat`	Update `C:\mmj2\test\windows\RunUnitTest7.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunUnitTest7.bat`. Note: don't bother manually saving the Command Window output -- it is not significant for UnitTest7. Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed.
`RunUnitTest8.bat`	Update `C:\mmj2\test\windows\RunUnitTest8.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunUnitTest8.bat`. Note: don't bother manually saving the Command Window output -- it is not significant for UnitTest8. Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed.
`RunUnitTest9.bat`	Update `C:\mmj2\test\windows\RunUnitTest9.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunUnitTest9.bat`. Note: don't bother manually saving the Command Window output -- it is not significant for UnitTest9. Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed.
RunUnitTest10.bat	Update `C:\mmj2\test\windows\RunUnitTest10.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunUnitTest10.bat`. Manually save the Command Window output to `C:\mmj2\data\result\UT10Err20061002a.txt` (using the date and suffix chosen for the test.) Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed.
RunUnitTest11.bat	Update `C:\mmj2\test\windows\RunUnitTest11.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunUnitTest11.bat`. Manually save the Command Window output to `C:\mmj2\data\result\UT11Err20061002a.txt` (using the date and suffix chosen for the test.) Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed. Compare output files stored in `c:\mmj2\data\gmfftest\althtml,c:\mmj2\data\gmfftest\html` and `c:\mmj2\data\gmfftest\myproofs`. They ought to match unless the software changed.
RunVolumeTest2a.bat	Update `C:\mmj2\test\windows\RunVolumeTest2a.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunVolumeTest2a.bat`. Note: don't bother manually saving the Command Window output -- it is not significant for VolumeTest2. WARNING: This test runs for at least 5 minutes AND sucks down 99% of the CPU! Be patient. Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed -- except for the elapsed time measurements reported because there are random variances in every run that are reflected in the output for theorems whose unification time is on the border between zero tenths of a second and one tenths of a second (the program truncates, and does not round output time durations.)
RunVolumeTest2b.bat	NOTE: Same as VolumeTest2 except that it exports ProofWorksheets using the new TMFF formatting (Format Nbr 3) and it uses the "Randomize" RunParm option (to make things even harder.) Not a problem except that a few minor differences may appear in parallel test results (for example: metcnp4lem2 may generate "soft" $d errors due to randomization of proof step hypothesis order and derivation of proof step formulas by the Proof Assistant.) Update `C:\mmj2\test\windows\RunVolumeTest2b.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002b`" = new software). Run `c:\mmj2\test\windows\RunVolumeTest2b.bat`. Note: don't bother manually saving the Command Window output -- it is not significant for VolumeTest2. WARNING: This test runs for at least 5 minutes AND sucks down 99% of the CPU! Be patient. Repeat test using new software (ie. output to "`20061002b`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed -- except for the elapsed time measurements reported because there are random variances in every run that are reflected in the output for theorems whose unification time is on the border between zero tenths of a second and one tenths of a second (the program truncates, and does not round output time durations.) Also, hypothesis Randomization will affect elapsed unification times for a certain number of theorems.
RunVolumeTest2c.bat	NOTE: Same as VolumeTest2 except that it exports tests the CompareDJs and UpdateDJs options of the ProofAsstBatchTest RunParm (to find Superfluous Mandatory $d statements in a .mm file. WARNING: This test runs for at least 15 minutes! Be patient. Update `C:\mmj2\test\windows\RunVolumeTest2c.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002c`" = new software). Run `c:\mmj2\test\windows\RunVolumeTest2c.bat`. Note: don't bother manually saving the Command Window output -- it is not significant for VolumeTest2. WARNING: This test runs for at least 5 minutes AND sucks down 99% of the CPU! Be patient. Repeat test using new software (ie. output to "`20061002c`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed -- except for the elapsed time measurements reported because there are random variances in every run that are reflected in the output for theorems whose unification time is on the border between zero tenths of a second and one tenths of a second (the program truncates, and does not round output time durations.) Also, hypothesis Randomization will affect elapsed unification times for a certain number of theorems.
RunVolumeTest2d.bat	NOTE: Same as VolumeTest2 except that its BatchTest RunParm uses the `DeriveFormulas` and `AsciiRetest` options. It also uses RunParms `ProofAsstDjVarsSoftErrors,GenerateReplacements and RecheckProofAsstUsingProofVerifier,yes` WARNING: This test runs for at least 10 minutes AND sucks down 99% of the CPU! Be patient. Update `C:\mmj2\test\windows\RunVolumeTest2d.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002c`" = new software). Run `c:\mmj2\test\windows\RunVolumeTest2d.bat`. Note: don't bother manually saving the Command Window output -- it is not significant for VolumeTest2. WARNING: This test runs for at least 5 minutes AND sucks down 99% of the CPU! Be patient. Repeat test using new software (ie. output to "`20061002c`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed -- except for the elapsed time measurements reported because there are random variances in every run that are reflected in the output for theorems whose unification time is on the border between zero tenths of a second and one tenths of a second (the program truncates, and does not round output time durations.)
RunVolumeTest2e.bat	NOTE: Same as VolumeTest2 except that its BatchTest RunParm uses the `DeriveFormulas,` `AsciiRetest` and `ProofAsstAutoReformat` (`no`) options. It also uses RunParms `ProofAsstDjVarsSoftErrors,GenerateReplacements and RecheckProofAsstUsingProofVerifier,yes`(Thus, it is identical to VolumeTest2d except that it adds "`ProofAsstAutoReformat,no`".) WARNING: This test runs for at least 10 minutes AND sucks down 99% of the CPU! Be patient. Update `C:\mmj2\test\windows\RunVolumeTest2e.bat` which contains a date-stamped file name with the correct date and suffix ("`20061002a`" = old software, "`20061002c`" = new software). Run `c:\mmj2\test\windows\RunVolumeTest2e.bat`. Note: don't bother manually saving the Command Window output -- it is not significant for VolumeTest2. WARNING: This test runs for at least 5 minutes AND sucks down 99% of the CPU! Be patient. Repeat test using new software (ie. output to "`20061002c`" output file). Compare output files stored in `c:\mmj2\data\result`. They ought to match unless the software changed -- except for the elapsed time measurements reported because there are random variances in every run that are reflected in the output for theorems whose unification time is on the border between zero tenths of a second and one tenths of a second (the program truncates, and does not round output time durations.)