fix: mainModuleName should use srcSearchPath

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.82k stars 325 forks source link

fix: mainModuleName should use srcSearchPath #4066

Closed digama0 closed 1 week ago

digama0 commented 2 weeks ago

As reported on Zulip. The mainModuleName was being set incorrectly when browsing lean core sources, resulting in failure of cross-file server requests like "Find References". Because the srcSearchPath is generated asynchronously, we store it as a Task Name which is resolved some time before the header is finished parsing. (I don't think the .get here will ever block, because the srcSearchPath will be ready by the time the initial command snap is requested.)

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):

❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-05-04 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. (2024-05-05 01:48:59)
✅ Mathlib branch lean-pr-testing-4066 has successfully built against this PR. (2024-05-08 02:04:12) View Log
✅ Mathlib branch lean-pr-testing-4066 has successfully built against this PR. (2024-05-08 03:12:41) View Log
✅ Mathlib branch lean-pr-testing-4066 has successfully built against this PR. (2024-05-08 10:03:51) View Log

Kha commented 1 week ago

@digama0 Marc and I were a bit concerned about the additional asynchronous control flow, so I pushed a refactoring that simplifies the whole context setup for the language processor. Makes sense?

digama0 commented 1 week ago

Yes, LGTM.