Unknown module prefix 'Batteries'

Stream: new members

[Labyrinth]

Hi.

I finally managed to install Mathlib in a project (turns out I just needed good enough wifi that the program wouldn't just straight up give up), however I am getting an error message that I don't have the technical knowledge to know how to fix (and some googling reveals nothing of use):

unknown module prefix 'Batteries'

No directory 'Batteries' or file 'Batteries.olean' in the search path entries:
c:\Users\me\.elan\toolchains\leanprover--lean4---v4.24.0-rc1\lib\lean

Any help?

[Labyrinth]

I forgot, I should probably mention: To setup Mathlib, I did what I undestand to be the standard steps:

• lake new <name of my project> math
• lake update (was redundant, but... why not I guess)
• lake build (seemed redundant again but whatever)
• Change the code to include an import Mathlib
• lake build again (and again seemed redundant)
• Open InfoView
• Error message above on the import Mathlib line

[Labyrinth]

Seems like it could be a VS Code thing?

I have a #check Even 0 line in my code to test if this works, and although the InfoView in VS Code is stuck at the error message above, the command line shows, after the second lake build:
info: DM1/Basic.lean:3:0: Even 0 : Prop

[Kevin Buzzard]

Just to be clear -- after lake new <name> math you changed directory into the project directory before doing all this lake update stuff?

Did you open the root directory of the project in VS Code (open folder not open file)?

Often a screenshot of VS Code with the file explorer open and the error displayed can help here.

[Labyrinth]

@Kevin Buzzard I did cd into the project directory (at first I hadn't but I realised my mistake). However, in VS Code, I opened the parent directory to the project directory, not the project directory itself

[Labyrinth]

Side note while my computer does its thing: Is it bad to have an import Mathlib instead of more specific imports for the specific things needed?

[Labyrinth]

It... works now? I couldn't tell you whether that's due to me opening the project directory instead of its parent directory, or any of the commands (same as last time) that I have put into the console but if it works it works I guess

[Labyrinth]

Going back to the project directory's parent folder, I get an Imports are out of date now, so I guess that was probably the issue

Edit: Nevermind, I get the same issue going back to opening the project directory directly. I give up trying to figure this out...

[Kenny Lau]

@Labyrinth can you upload your code to github?

1. create an empty new repository on github, with no README. say its name is <reponame>.
2. go to your project folder
3. git init
4. git add .
5. git commit -am "first commit"
6. git remote add origin https://github.com/<username>/<reponame>.git
7. git push -u origin master

[Labyrinth]

@Kenny Lau Sorry for being unclear in my last sentence. I meant that I was giving up trying to figure out what had happened exactly with my previous issue, not giving up trying to figure out how to make this work. In fact, it seems to all work as expected right now (opening the project directory and not a parent directory seems to have been the right fix for my case).

As of now I don't require further help (though I don't expect that to stay the case for long).

[Kevin Buzzard]

@Labyrinth if you don't open the root directory of the project with VS Code then it won't work -- VS Code won't see all the system files for the project containing the details of e.g. which version of Lean you're using (so it will use a random one), which modules you're depending on (so it won't be able to find Batteries) etc, so this was probably the problem.