Hi Noam, and welcome to the Metamath community!
Regarding contributing to set.mm, there are several amazing maintainers who can provide guidance far beyond what I can offer here. That said, here’s a general outline to help you get started: 1. *Fork the set.mm repository*: This creates your own copy to work on. 2. *Clone your fork locally*: Use git clone to download your forked repository to your machine. 3. *Create a branch*: Set up a dedicated branch for your new mathbox. 4. *Add your mathbox*: Insert an empty mathbox into set.mm following the conventions used by other contributors. 5. *Start with a simple theorem*: Add a small theorem to your mathbox. A good example could be a variation of an existing theorem from the main section, where a $d condition is replaced with a "non-free" hypothesis. 6. *Validate and format*: Run the provided bash scripts that invoke the Metamath program to validate and format your changes. These scripts are also used by GitHub Actions. 7. *Push to your fork*: Push your changes to your remote repository. 8. *Check GitHub Actions*: Verify if any errors are reported. If you encounter issues, feel free to share links to the errors here, and we’ll help you resolve them. 9. *Iterate*: Repeat the process until your branch passes all checks. 10. *Submit a pull request (PR)*: Once everything looks good, create a PR to propose your changes for review. With that, you’ll have your mathbox set up and ready for further contributions! Again, welcome to the gang—we’re glad to have you here! 😊 Glauco -- 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 visit https://groups.google.com/d/msgid/metamath/3f75bc6b-6a1a-437a-98dd-339ee53a22ddn%40googlegroups.com.
