error on "import tactic.ring"

Stream: new members

[agro1986]

Hi. I tried installing mathlib on MacOS based on the instruction here: https://github.com/leanprover-community/mathlib/blob/master/docs/install/macos.md

However when I typed import tactic.ring on my first line (in VS Code), the interpreter gives me

file 'tactic/ring' not found in the LEAN_PATH

invalid import: tactic.ring
could not resolve import: tactic.ring

Can anyone point me to the right direction? Thanks

[Bryan Gin-ge Chen]

Did you follow the directions in the projects doc?

[agro1986]

hmmm, let me check

[agro1986]

@Bryan Gin-ge Chen It works! thanks