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/d502b587-2a9d-4c53-b3b4-c944701fd64dn%40googlegroups.com.
