[Merged by Bors] - fix: do not keep only the first line of hints

[eric-wieser]

This is still not really the right approach, but it's clearly less wrong.

---

[github-actions]

PR summary 83558bf6b7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[adomani]

It looks reasonable to me. Should there be a test? Possibly one that involves trying a suggestion that would replace code followed by a comment, to make sure that the comment does not get mangled?

[kim-em]

Clear improvement! :-) Happy if you want to add a test, or not.

bors d+

[mathlib-bors]

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[adomani]

Suggested change

	| some m => pure <| SuggestionText.string ((← m.data.toString).drop 10)
	| some m => pure <| SuggestionText.string (((← m.data.toString).drop 10).dropWhile (· == '\n'))

Trying out an example, I think that it was drop, rather than take!

Maybe even trimLeft would be good.

[eric-wieser]

Do you have an example in mind where this has any effect?

[adomani]

I think that if you use the version in this PR you get

/--
info: Try these:
• ⏎
  trivial
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
example : 37 = 37 := by hint

while with the dropWhile you get

/--
info: Try these:
•   trivial
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
example : 37 = 37 := by hint

[eric-wieser]

I only see the second version with the PR in its current state, with

import Mathlib.Tactic.Hint

 -- newline to cause trouble, just in case!
register_hint
  trivial

/--
info: Try these:
• trivial
-/
#guard_msgs in
example : 37 = 37 := by hint

If newline really are ending up in the tactics, then i think it's the job of the register_hint'd tactic to not emit the newline in the first palce, not of hint to try to clean up.

[adomani]

When I tried this with the version in master, everything seems to work. I do not know what was happening before, but I am comforted by the fact that I did not dream this by the line-break character that #guard_msgs introduces automatically and that I certainly did not type myself!

[eric-wieser]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style