chore: remove the coercion from String to Name

[david-christiansen]

This coercion caused difficult-to-diagnose bugs sometimes. Because there are some situations where converting a string to a name should be done by parsing the string, and others where it should not, an explicit choice seems better here.

[david-christiansen]

This coercion has led to a number of subtle bugs and frustrating situations for me in the past. It seems to me that coercions make sense when there's a single canonical mapping from one type to another, where the target of the coercion is in some sense intuitively "the same". But in this case, there are two mappings, both of which make sense in different situations, and if I forget to use the correct one, I'd rather get a type error to remind me than a program that silently computes the wrong answer.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std CI can not be attempted yet, as the nightly-testing-2024-03-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-03-04 10:15:42)
• 🟡 Mathlib branch lean-pr-testing-3589 build this PR didn't complete normally. (2024-03-04 11:09:18) View Log
• 🟡 Mathlib branch lean-pr-testing-3589 build this PR didn't complete normally. (2024-03-11 12:53:41) View Log
• 🟡 Mathlib branch lean-pr-testing-3589 build this PR didn't complete normally. (2024-03-18 12:45:21) View Log
• 🟡 Mathlib branch lean-pr-testing-3589 build against this PR was cancelled. (2024-03-21 01:10:29) View Log
• 🟡 Mathlib branch lean-pr-testing-3589 build this PR didn't complete normally. (2024-03-21 02:08:05) View Log

[tydeu]

I added a bunch of stylistic suggestions for the changed code along with some tweaks for the Lake fixes.

[kim-em]

@david-christiansen, if you'd be able to rebase onto nightly-with-mathlib, that would be great. We have a recent compatible Mathlib build, and so I would like to see the scope of the downstream fallout (not necessarily immediately dealing with!) before we merge.

[david-christiansen]

OK, rebased on nightly-with-mathlib

[david-christiansen]

Thanks for the great feedback, @tydeu!

[tydeu]

@david-christiansen The speedcenter is failing because the Lake benchmark is using this coercion in its lakefile:

lean4/tests/bench/inundation/lakefile.lean

Lines 10 to 12 in 32dcc6e

	lean_lib Inundation where
	srcDir := "test"
	roots := #[test]

This can be changed to roots := #[.mkSimple test].

EDIT: Applied it myself to hopefully save you some time. 😄

[david-christiansen]

Applied it myself to hopefully save you some time. 😄

What a wonderful surprise, as I show up to do it! Thank you!

[kim-em]

Downstream changes look reasonable, so let's proceed:

• chore: don't use String->Name coercion, which may be removed leanprover-community/ProofWidgets4#48, and pushed v0.0.31
• chore: don't use String->Name coercion, which may be removed leanprover-community/quote4#39
• chore: don't use String->Name coercion, which may be removed leanprover-community/aesop#119
• chore: don't use String->Name coercion, which may be removed leanprover-community/batteries#705
• [Merged by Bors] - chore: don't use String->Name coercion, which may be removed leanprover-community/mathlib4#11556