Thierry asked (in my pull request): > I suppose that it has been obtained automatically? It's not explained in the mail on the group <https://groups.google.com/g/metamath/c/B9_PEy8YjU4/m/JCJPdz_RAQAJ?utm_medium=email&utm_source=footer>, but I'd be interested to know the process. Especially, is that something we can run periodically like minimize, or even within the checks?
Yes, I obtained shorter proofs automatically and by accident. I was testing my program (see the reference below) by converting proofs back and forth between different forms (compressed and table) expecting that I have to get an identical proof after all transformations if my program is correct. But it appeared that some proofs became longer and some shorter (while majority remained identical as expected, and two failed with an exception). I didn't have time to make sure what is the reason. That's why I have not mentioned this approach in my first email. But I am almost sure that the reason is as follows. My program always tries to reuse the first sub-proof for a statement. So, if a statement has two sub-proofs one longer and another shorter, the one which my program reads first will be reused instead of all other existing sub-proofs for that same statement. It is possible to create a JavaScript program and run it periodically, after changing the program to always reuse the shortest sub-proof :) On my laptop it ran about 3 minutes for set.mm. Unfortunately I don't have time right now for this change, since I am spending all my free time for developing of my proof assistant (metamath-lamp). But I will return to it once I am done with the proof assistant. The code I used to get shorter proofs - https://github.com/expln/metamath-lamp/blob/6a6cb4e23ce377406192bed25ffc83e1a4c46dcd/src/metamath/test/MM_save_proofs_to_files.res#L107 - Igor On Saturday, February 18, 2023 at 7:36:06 PM UTC+1 Benoit wrote: > Well, it appears that > https://github.com/metamath/set.mm/blob/develop/scripts/rewrap actually > implements the job described in > https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md. In > particular, it uses "save proof */compressed/fast". > But in the help of metamath.c, I see that this does reformatting but not > recompressing, so this expains that > https://us.metamath.org/mpeuni/19.41v.html remained strangely compressed. > > It's probably not worth it to remove the suffix "/fast" since the command > is then rather slow. I just made a PR which only does "MM> save proof > */compressed" and it should be enough to run it once in a while. The file > iset.mm was left unchanged and see the minimal diffs in the PR for set.mm. > (https://github.com/metamath/set.mm/pull/3046) > > Benoît > > On Saturday, February 18, 2023 at 2:15:59 PM UTC+1 Benoit wrote: > I saw in the zip file a shortening for 19.41v which was strange since the > label parts of the compress proofs were identical. Upon inspection, it > appears that the proof in set.mm was not compressed: I did > MM> sh pr 19.41v/c > and obtain you proof. > > Every submission should follow > https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md which was > not the case for that proof. I thought this was enforced but discovered it > is not: in > https://github.com/metamath/set.mm/blob/develop/.github/workflows/verifiers.yml#L123 > > you have only > - run: cp set.mm set-wrapped.mm > - run: scripts/rewrap set-wrapped.mm > - run: echo 'Checking for set.mm rewrapping:' && diff -U 0 set.mm > set-wrapped.mm > and https://github.com/metamath/set.mm/blob/develop/scripts/rewrap only > does, as its name indicates, part of the job described in > https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md. > > I'll open an issue. Ideally, we would do 'save proof */compressed' each > time, but this takes time, so we can do 'save proof */compressed/fast' > after one has done one initial sorrow 'save proof */compressed' and in > principle it should be sufficient. > > Benoît > > > On Thursday, February 16, 2023 at 10:36:03 PM UTC+1 David A. Wheeler wrote: > > > > On Feb 16, 2023, at 4:14 PM, Igor Ieskov <[email protected]> wrote: > > > > > Would you mind taking some steps so we can more easily review & add > them? > > > > Sure. I've just created a pull request. I will gradually update proofs > from the main part. I will not touch proofs from mathboxes. > > I suggest creating multiple pull requests. That way we can easily accept > some & not others. > > > > Below I am providing a list of owners of mathboxes for which I found > shorter proofs in order others not to download the file I attached (not > sure if posting full names is a good idea): > > AS > > AV > > GS > > JB > > NM > > RP > > TA > > WL > > That's fine, we know who they are. To be fair, > their public names are a terribly-kept secret, since they're posted in > <https://us.metamath.org/metamath/set.mm>. > If someone doesn't want to give their real name they can just give their > pseudonym (e.g., Mel L. O'Cat, Drahflow) or abbreviation (KP, ML), > though real names are great because I expect this database to outlive all > of us. > > --- David A. Wheeler > > -- 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/eaa318d7-bbd6-4abe-a624-1fa6ed21c784n%40googlegroups.com.
