feat: add warning for non-portable module names

[wkrozowski]

This PR adds a check for OS-forbidden names and characters in module names. This implements the functionality of modulesOSForbidden linter of mathlib.

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for b71df8f against e44351a are in. There are no significant changes. @wkrozowski

• ✅ build//instructions: -4.2M (-0.00%)

Small changes (1🟥)

• 🟥 build/module/Lean.Elab.Import//instructions: +326.5M (+13.47%) (reduced significance based on *//lines)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e44351add937efe4d286669ccd4c33023ca2e60e --onto 4f6bcc5adac8d6234a9e3def3675402cb89823c6. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-08 08:31:03)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-04-02 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-08 16:06:45)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e44351add937efe4d286669ccd4c33023ca2e60e --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-08 08:31:04)
• ✅ Reference manual branch lean-pr-testing-13318 has successfully built against this PR. (2026-04-08 16:13:21) View Log
• 🟡 Reference manual branch lean-pr-testing-13318 build against this PR didn't complete normally. (2026-04-08 16:14:15) View Log
• ✅ Reference manual branch lean-pr-testing-13318 has successfully built against this PR. (2026-04-09 11:06:31) View Log
• 🟡 Reference manual branch lean-pr-testing-13318 build against this PR didn't complete normally. (2026-04-09 11:07:29) View Log