Use project top-level for lsp-mode workspace root

[bustercopley]

When visiting a Lean file, lean4-mode adds the nearest ancestor directory containing a "lakefile.lean" to the lsp-mode's list of workspace root directories. If the file is in a package, this means lake will be started in the package directory, which is incorrect since it will cause lake to rebuild the files using the package's toolchain instead of the top-level project's. This commit tries to find the directory containing the top-level project's lakefile instead.

Notes:

• This commit doesn't check that the lakefile actually exists; it always will, for a normal lake project, but we might wish to check it anyway.
• lsp-mode's list of workspace root directories is persistent (it is stored in "~/.emacs.d/.lsp-session-v1"). Some users will already have package subdirectories in the list, and will still get workspaces with bad root directories. Perhaps we should remove any non-top-level package directories during the search, using lsp-workspace-folders-remove.

[bustercopley]

force-push: This originally used the existence of lake-packages to test if we are inside a child package. Since then, Lake has moved the packages directory to .lake/packages. I replaced the commit with a version that only uses the existence of lakefile.lean.

I tested the main use-case I had in mind:

1. Clear cached sessions: delete or rename ~/.emacs.d/.lsp-session-v1 before starting Emacs
2. Open a project that depends on Mathlib (by visiting any file that belongs directly to the project)
3. Wait for LSP mode to be ready (so the info-buffer is responding)
4. Check using M-x lsp-describe-session RET that the workspace root is the top-level directory of the project
5. Use M-., to go to the definition of something in Mathlib
6. Wait for LSP mode to be ready (so the info-buffer is responding)
7. Check using M-x lsp-describe-session RET that the workspace root is the top-level directory of the project (and not the Mathlib repo inside .lake/packages)

Also, repeat the entire recipe but visit a Lean file inside .lake-packages\mathlib\Mathlib first, and check the workspace root is still the project top-level directory (omit steps 2-4).

[bustercopley]

This can still be reproduced in master.

• Prepare a project and open a file in Emacs

git clone https://github.com/leanprover-community/mathematics_in_lean.git mil
cd mil
lake exe cache get
emacs MIL/C08_Groups_and_Rings/S02_Rings.lean

• Wait for the language server to finish initializing
• Toggle the infoview ([C-c TAB])
• Move point somewhere within MvPolynomial.eval ([M-< C-s mvpolynomial. RET])
• Go to the definition of MvPolynomial.eval by typing [M-.] to invoke the command xref-find-definitions
• The language server (lake) starts to build around 1000 Lean files; let it build a handful of them
• Stop the language server in "Mathlib/Data/MvPolynomial/Basic.lean" by typing M-x lsp-disconnect RET
• Switch back to the "MIL/C08_Groups_and_Rings/S02_Rings.lean" buffer
• Restart the file ([C-c C-d])
• The language server (lake) starts to build around 2000 Lean files.