Zulip Chat Archive

Stream: lean4

Topic: Configuring Time

Brent A Ritterbeck (May 11 2021 at 21:47):

I'm trying to get Lean4 to work on my Mac. I have VSCode running with the new Lean4 plugin; however, the InfoView just states "configuring mathlib4 0.1". I'm on the nightly build. Anyone else have this issue?

Mac (May 11 2021 at 21:48):

First, a clarification: are you using mathlib4?

Brent A Ritterbeck (May 11 2021 at 21:50):

Yes, I have pulled it down from Github, and I am entering at the root of the folder. In VSCode, I see the license, the .toml file, etc. in my navigation pane.

Mac (May 11 2021 at 21:51):

So the project you have open in VSCode is mathlib4?

Brent A Ritterbeck (May 11 2021 at 21:52):

Yes, that is correct. I am on commit 8ced11cf58c5aa6aab96726abf6c44896728d0b2.

Mac (May 11 2021 at 21:53):

Have you tried running leanpkg build on the command line? VSCode Lean 4 tends to want compiled oleans for a project before it starts working in my experience

Brent A Ritterbeck (May 11 2021 at 21:54):

@Mac Bingo, thank you.

Last updated: Dec 20 2023 at 11:08 UTC