From eef283485249d3a847e8f296d48de525fbdeab5b Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 23 Jan 2022 13:10:08 -0800 Subject: [PATCH 1/2] Add CONTRIBUTING.md file Most of the content here is adapted from various comments by various people on github issues and pull requests. It isn't intended to be a significant departure from how we have been working for the past month or so. --- CONTRIBUTING.md | 111 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 111 insertions(+) create mode 100644 CONTRIBUTING.md diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 00000000..e9eefdc5 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,111 @@ +# Contributing and Acceptance + +We're a friendly community, and we would love to have more collaborators! + +## Maintenance mode + +We view metamath-exe as being in maintenance mode. Although we do envisage +fixing bugs (at least serious ones) and making small updates to reflect +ongoing changes to our processes or metamath proof databases (especially +those in the https://github.com/metamath/set.mm repository), we do not +encourage developing significant new functionality in metamath-exe. + +Why? metamath.exe is the oldest of the metamath tools and is showing its +age in a lot of ways including that C is probably not the language that +anyone would choose for this kind of code today. + +Here's what Norm Megill, who wrote metamath-exe and did almost all of +its maintenance until 2021, said: + +> Another issue with the metamath program that people have requested is +> putting it on GitHub. However, strange as it may seem I actually don't +> want to encourage major contributions at this point in time. Almost +> every unsolicited patch I've been sent has had to be rewritten by me +> to fix memory leaks and other issues, and it can take a lot of my time +> to analyze them in complete detail. C is a dangerous language if you +> don't have intimate knowledge of all details of the program's data +> structures etc. If I put it on GitHub, I would dread having someone +> make a massive change that would require a week or more of my time +> to analyze. Ensuring bug-free code can take more time than it took +> to write it. (metamath mailing list, 2017) + +Although metamath-exe is now on github, we endorse the general sentiment +about hazards of making major contributions to metamath-exe. + +Are we saying we want no major contributions to metamath tools? Not at +all! Some work on metamath tools (for example, the only +implementation to date of the rather important definition checker) have been +done in [mmj2](https://github.com/digama0/mmj2) (although that code +has its own issues), and a lot of the recent work towards community +maintained metamath tools has focused on the +[metamath-knife](https://github.com/david-a-wheeler/metamath-knife) +verifier and/or tools built on top of it. + +Having said that, metamath.exe does a lot of things which are not covered +by other tools, and we expect that replacements, for example based on +metamath-knife, will not be written overnight. We aren't making a rigid +"never change metamath-exe" rule but we are saying that we expect such +changes will be primarily to tweak parts of metamath-exe which are getting +in our way, more so than expand what it can do. + +## Coding standards + +No need to worry about versions of the C language older than C99. +We would like to have our code usable by the +[CompCert C compiler](https://compcert.org/compcert-C.html) (as +described on that page it supports almost full C11, so this isn't +a big constraint). We think other compilers people are using probably +support C11 but if you want to use a feature not found in C99 +this might be work asking about in your pull request description. + +Some existing parts of metamath-exe have commented out code as a way of +showing alternative possibilities or old versions of the code. Now that +it is in git, we plan to remove most or all of this. + +We suspect some features of metamath-exe are being used lightly if at +all. We are potentially open to removing them to make maintenance +easier, but this should be done carefully (for example by proposing a +github issue, trying to find existing users, suggesting alternatives, +and the like). We'd hate to have this sort of thing prevent anyone +from upgrading to the latest version of metamath-exe. + +## What are the requirements for acceptance (merging)? + +We don't have as many automated checks on this repository as +would be ideal. So unless/until we add that, some of the following +may need to be checked manually. + +We expect all code merged to compile and not break existing +functionality. + +To be merged, a pull request must be approved by a different existing +contributor (someone who's already had some previous contributions accepted). +You can approve a change by viewing the pull request, selecting +the tab "Files Changed", clicking on the "Review Changes" button, +clicking on "Approve", and submitting the review. +You can also approve by using the comment "+1". +Feel free to approve something others have approved, that makes it clear +there's no serious issue. + +Once a pull request is approved (other than the person +originally proposing the change), any maintainer can merge it, +including the approver. +A maintainer is a member or owner of the Metamath GitHub organization. + +We especially encourage discussion and, perhaps, letting a bit of time +pass before merging, if a change seems large or risky (given the general +philosophy described in the "Maintenance mode" section above). + +We encourage changes to be smaller, focusing on a single logical idea. +That makes changes much easier to review. +It also makes it easy to accept some changes while not accepting others. + +The following people are active and are willing to be contacted +concerning metamath-exe. Please propose a change to this file if you want +to be listed here. + +* Mario Carneiro (@digama0) + +## For more information + +For more general information, see the [README.md](README.md) file. From 99a136b91a228c5777aaf0280093f4bffb2720f9 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 23 Jan 2022 14:08:02 -0800 Subject: [PATCH 2/2] say why Norm isn't maintaining it Co-authored-by: Mario Carneiro --- CONTRIBUTING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index e9eefdc5..f03e7a05 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -15,7 +15,7 @@ age in a lot of ways including that C is probably not the language that anyone would choose for this kind of code today. Here's what Norm Megill, who wrote metamath-exe and did almost all of -its maintenance until 2021, said: +its maintenance until his passing in 2021, said: > Another issue with the metamath program that people have requested is > putting it on GitHub. However, strange as it may seem I actually don't