I probably can't help that much, but I would encourage you to structure that as a CI script and make a PR to set.mm to run it in CI.
On Mon, Jun 17, 2024 at 12:03 AM [email protected] < [email protected]> wrote: > > in the long term we might want [...] proof verification > > we should have verification that the proofs in the file are actually > correct, and while we're at it we may as well also ensure they have the > claimed length > > The initial purpose of pmGenerator (before it even had that name) was to > convert all proofs in pmproofs.txt into formula-based proofs, and validate > them along the way. > > So, whenever a proof database is parsed, this comes with automated > validation, and when reassembled, its proof steps are counted automatically > and printed into the output file. > Thus an easy way to verify both correctness and lengths is to reassemble > pmproofs.txt via '-a' without applying any replacements (i.e. referring to > an empty replacements file), like > > $ ./pmGenerator -a XY empty.txt pmproofs.txt pmproofs-reassembled.txt -l > -d -w > > and then comparing 'pmproofs.txt' with 'pmproofs-reassembled.txt' to > compare specified proof lengths. > > The program should throw an error when any proofs are incorrect (if not, > that'd be an issue <https://github.com/xamidi/pmGenerator/issues>), and > otherwise the user can subsequently check whether the result is the same as > in the original file, excluding the header. > For example, by pasting the contents of both files to a site such as > https://www.textcompare.org/. > > All file versions provided by me are verified by the tool, due to how they > were processed and generated. > > Exemplary output: > $ ./pmGenerator -a XY data/empty.txt data/pmproofs.txt > data/pmproofs-reassembled.txt -l -d -w > Sun Jun 16 22:00:03 2024: Process started. [pid: 48532, tid:1] > Tasks: > 1. applyReplacements("XY", "data/empty.txt", "data/pmproofs.txt", > "data/pmproofs-reassembled.txt", false, true, true, true) > > [Main] Calling applyReplacements("XY", "data/empty.txt", > "data/pmproofs.txt", "data/pmproofs-reassembled.txt", false, true, true, > true). > 0.27 ms taken to read 0 shortening replacements and 0 styling replacements. > 1.14 ms taken to read 196 condensed detachment proofs from file > "data/pmproofs.txt". > 0.00 ms taken to store 196 lengths. > 0.03 ms taken to apply replacements. > 202.27 ms taken to check, generate and save 54594 bytes of MM-styled > condensed detachment proofs (0 shortened, 0 styled, 196 unmodified) to > data/pmproofs-reassembled.txt. > Sun Jun 16 22:00:03 2024: Process terminated. [pid: 48532, tid:1] > > Note: Omitting the '-w' will remove all line wrappings, which can make > the individual D-proofs easier to use. > > PS: Isn't drule.c (mentioned in the file's header) also able to validate > all proofs in the file at once? I mean, it should, but maybe it just > ignores some issues that can be ignored, like incorrectly lining up > multiple correct D-proofs > <https://github.com/xamidi/pmGenerator/blob/1.2.0/metamath/DRuleParser.cpp#L1028> > .. > > > [email protected] schrieb am Sonntag, 16. Juni 2024 um 19:29:57 UTC+2: > >> While I agree, this is a nontrivial task because pmproofs.txt is not a >> metamath database at all, it's a completely unrelated format which needs >> bespoke tools to process it. But I agree that we should have verification >> that the proofs in the file are actually correct, and while we're at it we >> may as well also ensure they have the claimed length. >> >> On Sun, Jun 16, 2024 at 12:26 PM Gino Giotto <[email protected]> >> wrote: >> >>> I think in the long term we might want to treat 'pmproof.txt' as a >>> proper database; involving proof verification, markup verification, and >>> essentially the important features already implemented for the main ones. >>> It seems there is enough interest for this project, but Metamath users >>> might not even know that it exists as it is somewhat hidden both on the >>> webpage and on Github. For example, in 2023 an user attempted >>> <https://github.com/metamath/set.mm/pull/3622>to submit a shorter proof >>> back to the axioms in set.mm, but the revision was not accepted because >>> it was longer in the compressed format. I think this confusion can be >>> avoided by integrating the pmproof.txt database into the set.mm >>> repository (perhaps into a Metamath Solitaire folder?), and add it to the >>> table of databases at the beginning of the Metamath front page (although a >>> Metamath Solitaire explorer might need to avoid showing the proof formulas, >>> as they tend to be very long). >>> Il giorno domenica 16 giugno 2024 alle 03:53:59 UTC+2 >>> [email protected] ha scritto: >>> >>>> I have found an additional 40 shorter proofs for >>>> https://us.metamath.org/mmsolitaire/pmproofs.txt. See 'pmproofs.txt' >>>> at https://github.com/xamidi/mmsolitaire [changes: f9a40e7 >>>> <https://github.com/xamidi/mmsolitaire/commit/f9a40e79bf8764c11b1b891eae58c2fdbce15293> >>>> ]: >>>> *2.32: 91 -> 83 >>>> *3.3: 59 -> 55 >>>> *3.33: 95 -> 73 >>>> *3.34: 105 -> 73 >>>> *3.43: 117 -> 109 >>>> *3.44: 181 -> 161 >>>> *3.47: 203 -> 199 >>>> *3.48: 241 -> 171 >>>> *4.14: 283 -> 263 >>>> *4.15: 277 -> 233 >>>> *4.32: 317 -> 313 >>>> *4.33: 207 -> 199 >>>> *4.38: 585 -> 529 >>>> *4.39: 479 -> 465 >>>> *4.4: 355 -> 345 >>>> *4.41: 249 -> 241 >>>> *4.52: 219 -> 209 >>>> *4.53: 169 -> 159 >>>> *4.72: 195 -> 193 >>>> *4.76: 249 -> 241 >>>> *4.77: 285 -> 265 >>>> *4.82: 175 -> 157 >>>> *4.83: 245 -> 231 >>>> *4.85: 121 -> 119 >>>> *4.86: 555 -> 551 >>>> *4.87: 447 -> 439 >>>> *5.15: 267 -> 185 >>>> *5.16: 333 -> 331 >>>> *5.18: 503 -> 491 >>>> *5.23: 513 -> 501 >>>> *5.33: 389 -> 343 >>>> *5.35: 159 -> 145 >>>> *5.53: 673 -> 633 >>>> *5.54: 239 -> 233 >>>> *5.6: 167 -> 163 >>>> *5.61: 259 -> 249 >>>> *5.62: 167 -> 157 >>>> *5.74: 337 -> 335 >>>> *5.75: 351 -> 331 >>>> biass: 1877 -> 1851 >>>> >>>> For this, I used a new "proof compression" feature (parameter '-z' for >>>> '--transform') of pmGenerator <https://github.com/xamidi/pmGenerator> >>>> (to be released in version 1.2.1), >>>> which was mainly inspired by Gino Giotto from this comment >>>> <https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-9769069> >>>> and his corresponding solution. >>>> >>>> While Gino (to my surprise) found an argument that could be replaced by >>>> an axiom (technically, by any theorem), >>>> only 1 out of 69 elementary improvements for pmproofs.txt was of that >>>> nature, all others were replacements of one or both inputs of a D-rule with >>>> proofs of non-trivial theorems. >>>> >>>> Indeed, the feature does not only test for axioms but for all formulas >>>> that occur in a proof summary, and tries all combinations of such formulas >>>> as arguments of a D-rule, as long as the overall result would be shorter >>>> than before. >>>> >>>> The compression took roughly five and a half hours and was based on >>>> 'pmproofs-summary.txt', which I shared a few months ago on this >>>> mailing list >>>> <https://groups.google.com/g/metamath/c/eHW5779KfXU/m/A2WAkOamAQAJ>. >>>> (It usually takes only a few seconds to minutes for proof summaries of >>>> reasonable size, but pmproofs' collection is rather large.) >>>> More details — which commands I used and what output they gave — can be >>>> seen in the appendix ('pm-z-improvements.log'). >>>> >>>> The new feature also led to quite a few more improvements >>>> <https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-9784395> >>>> of the minimal C-N 1-base challenge. >>>> >>>> Thanks to Gino for the inspiring and motivating comments. :-) >>>> >>>> >>>> — Samiro Discher >>>> >>>> -- >>> You received this message because you are subscribed to the Google >>> Groups "Metamath" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to [email protected]. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/metamath/6029d44d-d5a3-4692-b992-f4754a312629n%40googlegroups.com >>> <https://groups.google.com/d/msgid/metamath/6029d44d-d5a3-4692-b992-f4754a312629n%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/22617d1f-2d29-4698-b090-720ad1529909n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/22617d1f-2d29-4698-b090-720ad1529909n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvjO_kicmtnZSs%2B08iJNybDiJDH_SuwhuwQgTh3Xxj7bg%40mail.gmail.com.
