docs: Adding CONTRIBUTING.md

.github/copilot-instructions.md

@@ -0,0 +1 @@
+Read `CONTRIBUTING.md` for guidelines on contributing to this project.

CONTRIBUTING.md

@@ -0,0 +1,35 @@
+# Contribution
+
+## Commit convention
+
+Follow usual conventional commit for PR title (we always squash merge).
+
+```
+<type>(scope): <subject>
+```
+
+Choose `<type>` from below (should be one, but like `fix/doc` might be ok).
+- `add`: Adding new results, definition, theorems.
+- `fix`: Fixing existing results for something misformalized
+- `refactor`: Rename and organize definitions/theorems. (essentially nothing changed about existing facts.)
+- `doc`: Adding or updating documents.
+- `ci`: Configure GitHub Actions.
+- `chore`: Maintaining other things (ex: version-up).
+
+`scope` is optional, specify like `FirstOrder`, `Modal` if needed.
+
+## Usual commands
+
+### Build
+
+```shell
+lake build Foundation
+```
+
+### References
+
+Format [references.bib](./references.bib) when adding references.
+
+```
+bibtool -r .bibtoolrsc -i references.bib -o references.bib
+```

README.md

@@ -108,18 +108,9 @@ Automatically generated[^1] diagrams "Zoo", illustrate the Lean4-verified interr
 
 ![Interpretability Logic Zoo](https://formalizedformallogic.github.io/Zoo/interpretability_logic.png)
 
-## Build
-
-```shell
-lake build Foundation
-```
-
-## References
-
-```
-bibtool -r .bibtoolrsc -i references.bib -o references.bib
-```
+## Contributing
 
+For instructions on how to build the project, run tests, and contribute, see [CONTRIBUTING](./CONTRIBUTING.md).
 ## Developers
 
 List of contact information and areas of expertise of the current main developers.