Copy module name to clipboard

[alreadydone]

Given a file mathlib4/aaa/bbb/ccc.lean open in VSCode, I'd like to one-click copy the string aaa.bbb.ccc to the clipboard. This is useful if you want to import the current file in another file, or if you want to run lake build aaa.bbb.ccc in the terminal (sometimes if you build the file by restarting it, the progress may not be displayed.) This feature could be implemented as a command (possibly called Lean 4: copy module name) which one can select after hitting Ctrl+Shift+P.

Zulip

[mhuisi]

Note that in general, converting a file path to a module name requires the Lean search path (also as mentioned in the thread you linked) because Lake allows configuring the library root. I don't know of any way to extract that information from Lake (cc: @tydeu).

We could still provide a heuristic that works for libraries with the default root configuration, though.