Submitting a theorem to set.mm

[Larry Lesyna]

I am ready to submit my first theorem to Metamath. I tested it in my local copy of set.mm and I have created a personal fork.  I could submit a pull request, but I think it would be better if my submission could be reviewed before doing so.  I appreciate any advice.

Larry

[Jim Kingdon]

First of all, welcome! Always good to have more people doing things with metamath.

Various people would be glad to look at your submission but I think making it a pull request will be the easiest way to let them look at the change. I mean you could make it a Draft Pull Request if you really want to emphasize the point of not being sure whether it should be merged.

This also means the automated checks will run which covers a lot of points.

[David A. Wheeler]

> On Jul 17, 2023, at 5:21 PM, Larry Lesyna <lesy...@gmail.com> wrote:
>
> I am ready to submit my first theorem to Metamath. I tested it in my local copy of set.mm and I have created a personal fork. I could submit a pull request, but I think it would be better if my submission could be reviewed before doing so. I appreciate any advice.

WONDERFUL! We're always delighted to have new contributors.
Jim Kingdom gave some great advice. Welcome aboard!

--- David A. Wheeler

[Mázsa Péter]

Welcome! One more optional step to diminish the natural stress of the
first public commit: after you commit to your origin at Github
https://github.com/lesyna/set.mm/
but before you commit to the upstream, as Jim wrote, your first draft
pull request to
https://github.com/metamath/set.mm/
from your origin, you can check in relative privacy, still in your
cloned repo, here
https://github.com/lesyna/set.mm/actions/workflows/verifiers.yml
whether all your verifiers will pass = be green.

P.

> --
> 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 metamath+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ADE2F615-6313-4B94-BF57-18634E6ECCB3%40dwheeler.com.

[llesyna]

Done! My submission passed verification when using my local repo, and passed all verifiers except metamath.exe when I did the pull request. I appreciate the advice and please let me know what to do next, if necessary.

Larry