How to actually use mathlib4?

Stream: new members

[debord]

I followed the instructions of mathlib4 and used make to build mathlib4 and made a new project with mathlib4 as a dependency with lake new project math but it seems I still cannot import anything from mathlib4 in VS code. import Mathlib.Data.Real.Basic gives unknown package 'Mathlib'. I can't find any documentation that seems to point to what I'm missing.

[David Renshaw]

In case it helps, here is an example project that successfully imports mathlib4: https://github.com/dwrensha/math-puzzles-in-lean4

[debord]

I cloned this and am still getting unknown package 'Mathlib' so clearly something is misconfigured on my end. I thought it had to do with the fact that I have VS installed from a Flatpak and it was trying to search for mathlib4 only in the Flatpak sandbox, but running one of your files in terminal outside of the Flatpak environment still gives Bulgaria1998Q8.lean:1:0: error: unknown package 'Mathlib'.

Edit: I'm also getting this still in the mathlib4 source code itself. Seems like using make in the mathlib4 directory didn't even build anything.

[David Renshaw]

lake build in the project root is what I do

[debord]

Okay, that built a bunch of mathlib stuff again, and seemingly did nothing. Still my output in VS code is unknown package 'Mathlib', and trying to run one of the .lean files gives the same thing. Am I even doing this right? What exactly is building the files even doing?

[David Renshaw]

have you tried closing and reopening vscode?

[debord]

Yes, of course. Did not work.

[David Renshaw]

is it possible that vscode is trying to use lean 3 instead of lean 4?

[debord]

I have the lean4 extension installed. I shouldn't have lean 3 anything on my machine as far as I'm aware.
Edit: Does anyone know of a way to get more verbose error output?

[debord]

Figured it out. It seems it has something to do with this 'workspaces' thing in VS. I had everything just in a 'lean' workspace with the various folders in it. When I closed that workspace and then opened just the math-puzzles-in-lean4 folder as its own workspace, it works and detects Mathlib without errors.