I added links to "How can I contribute to Metamath?" ( http://us2.metamath.org/index.html#contribute ) near the top of these pages: http://us2.metamath.org/mpeuni/mmset.html http://us2.metamath.org/mpeuni/mmrecent.html
I also added links to the wiki https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing and CONTRIBUTING.md under "How can I contribute to Metamath?". Hopefully this will address most of your concerns. Feel free to enhance the wiki if you wish. Norm On Sunday, September 22, 2019 at 11:32:46 AM UTC-4, savask wrote: > > So we encourage (but do not require) that people minimize their proofs >> when it is not too much trouble to do so. >> > > Perhaps it is a bit off-topic for this thread, but I think it's worth > suggesting anyway. > Maybe there should be a "tutorial" page for contributing to set.mm which > will explain all the steps required and some tips/suggestions (like > minimizing your proof before contributing it to set.mm)? I imagine a > set-by-step explanation, showing how to transfer the statement and the > proof of your theorem into set.mm, how to comment it correctly, how to > minimize the proof, wrap/unwrap and so on. > > It seems to me that set.mm accumulated a baggage of rules and conventions > (some of which are, of course, covered in the "Conventions and Style" > page), so having a definite first guide will make contributing more > "user-friendly" and will encourage correct behavior, like minimizing > theorems or writing detailed comments. > -- 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/02a6d7be-b4d5-4dee-9337-db39c1f33fe5%40googlegroups.com.
