General information about installing and using libs?

Stream: new members

[mars0i]

Is there a web page or blog post that gives a big picture and general details about how to install and use libraries? I'd also be interested in overview documentation on lake. There are lots of great resources for newbies at https://lean-lang.org/documentation and https://leanprover-community.github.io/learn.html. lake is easy to use to get started on a project even if you don't understand everything it sets up, and the default lake help info at the command line is somewhat useful.

But I haven't found any source that answers questions like the following. That doesn't mean the information isn't there somewhere, but I've looked quite a bit and have had trouble finding it. I think I know the answers to most of the following questions, now, but I was guessing, and I'm not sure.

Since there is some documentation on using libraries linked from the main Lean website, maybe it would help if I mentioned some of the questions I have, to clarify what was missing from the materials I did find. The rest of this post contains those questions (mostly answered for myself, at this point, but with some difficulty).

---

The std4 README says:

To use std4 in your project, add the following to your lakefile.lean:
require std from git "https://github.com/leanprover/std4" @ "main"

I have done that, but what does it do? After I examine a source file in a Lean-enabled editor (I'm using lean.nvim) from a directory containing such a lakefile.lean, is std4 installed on my system? Where is it? I eventually found that in .lake/packages under the project directory that lake created.

My next question was where I need to be implement the instructions in the std4 README for generating std4's docs? It looks like the right place to be is .lake/project/std/.lake, but this was not obvious.

Then should I just use the index.html that's under build then? Is there any way to access documentation on specific functions and data structures via LSP?

I also wasn't sure about the exact syntax for naming a module in an import statement. I think I've figured out that for std4 or mathlib4, it should be e.g. Mathlib.Data.Vector, i.e. the full path displayed at the top of the documentation page for a module.

Thanks!