feat: public imports for environment linters inside of lake lint in module system mode

[wkrozowski]

This PR makes lake lint --builtin-lint import module-system targets at the public (OLeanLevel.exported) level instead of private. Environment linters now lint the public surface of such modules, matching how downstream consumers see them. Non-module targets retain their previous behaviour (private level), and text-linter warnings recorded via lintLogExt are preserved across the level change because that extension stores uniform OLean entries.

The top-level module's .olean is peeked via findOLean + readModuleData to decide whether to use .exported or .private, mirroring processHeaderCore. A new tests/lake/tests/builtin-lint-module/ test exercises the new code path with a dummy env linter and verifies that text-linter warnings on both public and private definitions survive the level switch.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-25 18:12:41)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13843 has successfully built against this PR. (2026-05-25 19:13:13) View Log