Error creating new project

Stream: general

[Daniel Donnelly]

My goal is to import stuff from mathlib.

pasted image
That's the step that I get to according to the instructions:

Working on an existing package

If you have not logged in type
    source ~/.profile.

Clone the repo of the project you want to get

Cd to the project folder

Type
    leanpkg configure
to get leanpkg ready

python $HOME/.mathlib/bin/update-mathlib

Type
    leanpkg build
to compile everything, this will take some time.

launch VScode, either through your application menu or by typing code

On the main screen, or in the File menu, click "Open folder"

Choose the folder lean-perfectoid-spaces (not one of its subfolders).

[Simon Hudon]

The long number it gives you is a commit of mathlib. On github, go to that commit to make sure that it exists

[Daniel Donnelly]

I'm creating it from scratch. Now intellisense shows that algebra.CommRing is there (in dropsown) but it results in import error still:

[Daniel Donnelly]

pasted image

[Daniel Donnelly]

I followed instructions here: https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md

[Daniel Donnelly]

Now there's no error red zigzag line, however, it's taking a long time to update Messages (hasn't updated even yet)

[Daniel Donnelly]

Lean is working now, it's just updating in the bg (?)

[Daniel Donnelly]

It's working now :D

[Daniel Donnelly]

import algebra.all

I also needed to run the mk_all.sh script from where it is placed by leanpkg