Small bugs in core?

Stream: lean4

[Thomas Murrills]

What's the right thing to do when seeing a small bug in core? (Example at hand: I noticed a missing s! in front of a clearly-intended-to-be-interpolated string that's used for an error message.)

The contribution guidelines say that "simple fixes for typos and clear bugs are welcome", but follows that with a request to hold off on submitting PRs for now. Which takes priority in a case like this? (And if the simple fix does, does a simple fix for a clear, minor bug like this entail an issue + a PR, or just a direct PR, since the bug is so small?)

Likewise, I occasionally notice small, non-meaningful typos in core docstrings. Would fixing a single typo like that in a PR be welcome? (I could, alternatively, hang onto them and submit several docstring typo fixes in a larger PR—or simply ignore them.)

My goal here is just to not make unneeded noise, since I know everyone working on core is very busy. At the same time, I thought maybe I could help when I notice something like this. :)

[Mario Carneiro]

small bugs I would just PR, I wouldn't expect much drama about that

[Mario Carneiro]

typos too

[Thomas Murrills]

Cool—is chore: appropriate in the PR title/commit msg to indicate these would be small PRs, or is fix:/docs: the way to go?

[Mario Carneiro]

fix: for the bugfix, not sure about fix: vs docs: for typos

[Mario Carneiro]

historical evidence points to doc:

[Thomas Murrills]

Also—I'm guessing something like this doesn't warrant adding a test, right?

[Mario Carneiro]

it's probably fine

[Arthur Paulino]

For a bug fix I would take the extra effort to write at least a test that exercises it. Tests are not just to show that your fixes work, but also to guarantee that the behaviors you're testing won't regress in the future.

[Scott Morrison]

For the example above (adding a s! or m! to a string that is clearly intended to use interpolation), I think a test would be unnecessary overhead. But yes, please err on the side of testing. :-)