lake: import error points at wrong line

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When importing some non-installed module, the error message points at line 1 even if the bogus import is in a later line.

Context

n/a

Steps to Reproduce

1. Create a new lean project (lake new) and then use the following source code:

import Lean
import Qq

2. Run lake build

Expected behavior: Qq is not declared as a dependency, so it should point at line 2 to complain about the import.

Actual behavior:

✖ [2/10] Building ReflectionExample.ReflectAttr
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH= /home/r/.elan/toolchains/stable/bin/lean ././././ReflectionExample/ReflectAttr.lean -R ./././. -o ././.lake/build/lib/ReflectionExample/ReflectAttr.olean -i ././.lake/build/lib/ReflectionExample/ReflectAttr.ilean -c ././.lake/build/ir/ReflectionExample/ReflectAttr.c --json
error: ././././ReflectionExample/ReflectAttr.lean:1:0: unknown module prefix 'Qq'

No directory 'Qq' or file 'Qq.olean' in the search path entries:
././.lake/build/lib
/home/r/.elan/toolchains/stable/lib/lean
error: Lean exited with code 1

The error points at 1:0, i.e. line 1, column 0. But that's the position of import Lean, which is actually fine, the problem is in line 2.

Versions

Locally:
Lean 4.15.0
Target: x86_64-unknown-linux-gnu

Occurs with latest Lean on https://live.lean-lang.org/#project=lean-nightly&codez=JYWwDg9gTgLgBAGQKYEMB2AoUlZwIoCOGQA

Additional Information

n/a (hopefully ;)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the issue in a new Lean project with the two imports shown in the issue, then run lake build and inspect how the missing Qq module diagnostic is assigned its source position. The fix is complete when the diagnostic points to line 2, column 0 for the undeclared import without changing the valid import Lean result.