lake: specify conflict semantics for `require X with <opts>` when X is required twice

require X from … with <opts1> and require X from … with <opts2> are both legal in different lakefiles that resolve to the same dependency X. Lake currently loads a given package once per workspace, so one configuration wins and the other is silently discarded. Which one wins, and whether the user gets any diagnostic, is not documented.

Plausible policies:

• First-merge wins (whichever require Lake encounters first during dependency resolution).
• Root-closest wins (the require nearest to the workspace root in the dependency graph takes precedence; ties broken deterministically).
• Structural merge (per-key merge; conflicting keys are an error). Hard with arbitrary NameMap String.
• Error on conflict (with a way to opt out per-require).

The right call depends on how Lake maintainers want users to think about cross-package configuration. Whatever the choice, it should be (a) documented in the README and Dependency.opts doc-string, (b) detectable at config-resolution time, and (c) surfaced as either a warning or a diagnostic when two parents disagree.

Filing this as a design issue so the companion docs PR (https://github.com/leanprover/lean4/pull/14004 sibling — separate PR following) can land without blocking on the answer.

Concrete instance that surfaced this: https://github.com/leanprover/lp/pull/172 needed lp to forward leanLibDir into both SoplexFFI and LPBackendSoplexFFI, and the latter has its own internal require SoplexFFI with {} — which one wins for the workspace-wide SoplexFFI instance was not obvious.

🤖 Prepared with Claude Code

Start by reviewing the README and the Dependency.opts doc-string, then trace how Lake resolves repeated requirements at config-resolution time. A decision is complete when one conflict policy is specified, disagreement detection and warning or diagnostic behavior are defined, and the chosen semantics are documented.