search

digama0 / mmj2

mmj2 GUI Proof Assistant for the Metamath project
GNU General Public License v2.0
72 stars 24 forks source link

ProofAsstExportToFile in UT2PA001.txt is missing 7th parameter?? #55

Closed billh0420 closed 2 years ago

billh0420 commented 3 years ago

I am running on a Mac and I am trying to run some of the tests in the test/windows folder (after making suitable changes).

In particular, I am trying RunUT2.bat which uses the UT2PA001.txt param file. The UT2PA001.txt is in folder mmj2/data/runparm/windows. Line 28 of that file is:

   ProofAsstExportToFile,dfbi2,dfbi2.mmp,update,un-unified,NotRandomized,Print

When I try to run it, I get an error for that line that it needs a 7th parameter like DeriveFormulas. If I add this parameter at the end, the error goes away.

Question: Is this a true error?

Note: If you do a search on "ProofAsstExportToFile," there are other places that lack this 7th parameter. I found 4 and possibly 5 such cases. That are other cases which have the parameter provided.

digama0 commented 3 years ago

It's probably an error. I've never used the files you are talking about, nor have I ever used ProofAsstExportToFile, so I wouldn't be surprised if one or the other is out of date.