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/a639467f-9dd5-4872-a787-95bc634a041fn%40googlegroups.com.
