How does one create a lean project and have mathlib import work when not creating the lean project at the $HOME directory?

Question

I want to create a lean project inside another folder besides the $HOME folder. So I was going through the official Creating a Lean project instructions on how to create a Lean Project, but it only works (i.e., the import to mathlib) only works if I do the instruction on $HOME.

So for example the instructions say:

Go to a folder where you want to create a project in a subfolder my_project, and type lake +leanprover/lean4:nightly-2023-02-04 new my_project math.

but when "go to a folder" is anything but the root it doesn't work.

I wrote a bash file for what the instructions say,

1. one were it works (the one at $HOME) and

2. one that doesn't work (when I try to create the lean project not at $HOME):

Project Creation works when doing instructions at $HOME

# -- Go to a folder where you want to create a project in a subfolder my_project, and type lake +leanprover/lean4:nightly-2023-02-04 new my_project math.
cd $HOME
lake +leanprover/lean4:nightly-2023-02-04 new my_project math
# if you get an error message saying lake is an unknown command and you have not logged in since you installed Lean, then you may need to first type 
# source ~/.profile or source ~/.bash_profile
# - Go inside the my_project folder and type lake update, then lake exe cache get and then mkdir MyProject.
cd my_project
lake update 
lake exe cache get
mkdir MyProject
# Your Lean code should now be put inside files with extension .lean living in my_project/MyProject/ or a subfolder thereof.
cd MyProject
touch Test.lean
echo 'import Mathlib.Topology.Basic\n\n#check TopologicalSpace' > Test.lean

Project Creation fails anywhere else e.g., inside a $HOME/entire_project_root

mkdir $HOME/entire_project_root
# -- Go to a folder where you want to create a project in a subfolder my_project, and type lake +leanprover/lean4:nightly-2023-02-04 new my_project math.
cd $HOME/entire_project_root
lake +leanprover/lean4:nightly-2023-02-04 new my_project math
# if you get an error message saying lake is an unknown command and you have not logged in since you installed Lean, then you may need to first type 
# source ~/.profile or source ~/.bash_profile
# - Go inside the my_project folder and type lake update, then lake exe cache get and then mkdir MyProject.
cd my_project
lake update 
lake exe cache get
mkdir MyProject
# Your Lean code should now be put inside files with extension .lean living in my_project/MyProject/ or a subfolder thereof.
cd MyProject
touch Test.lean
echo 'import Mathlib.Topology.Basic\n\n#check TopologicalSpace' > Test.lean

Is this the expected behaviour?

The error message is:

Test.lean:1:0
unknown package 'Mathlib'

---

Comment on version 2023-02-04

@FrançoisG.Dorais quoting the official instructions/documentation: Do not worry about the date in the previous command, it ensures you will use a sufficiently recent version of lake but has no impact on the version of lean your project will use https://leanprover-community.github.io/install/project.html#creating-a-lean-project so idk, I'm just reading them and following what the lean maintainers tell me to do. I agree with you at first glance.

Answer 1

Your screenshot indicates that you are opening VS Code in $HOME. You need to open the root directory of the project folder instead. For example on the command line you need to run code . in the directory $HOME/entire_project_root/my_project, and in point-and-click VS Code you need to go to File -> Open Folder -> (open the folder called my_project). Then the imports will work.

The reason is that VS Code looks for information about which versions of things like Lean and Mathlib to use in any given project, in the system config files for the project, which it expects to find in the directory which you've opened in VS Code. Mathlib typically updates about 20 times per day right now, so two distinct projects which depend on mathlib will with very high probability use distinct versions of mathlib.

Observe the subtle difference between my screenshot and yours at the top:

Answer 2

To make it easier to find what I did. I don't exactly know how Lean & vscode are setup such that vscode knows the path to the right Lean4 toolchain (e.g., compiler etc.), the "Lean env for the libraries", etc., but what I did is what Kevin suggested:

1. Click the icon and then use "file" -> "open folder" and open the project folder, not the root folder. If you need more precise help then you should just ask on the Lean Zulip. VS Code needs to know which version of Lean and mathlib you're using [Kevin B.]. In particular open my_project from the Lean code example that (confusingly) has my_project/MyProject/Test.lean.

2. if it doesn't work restart (update) vscode. That seemed to work for me. Perhaps setting up the project from the vscode intergrated terminal confuses vscode.

This is the code I ran:

# -- Go to a folder where you want to create a project in a subfolder my_project, and type lake +leanprover/lean4:nightly-2023-02-04 new my_project math.
cd $HOME
lake +leanprover/lean4:nightly-2023-02-04 new my_project math
# if you get an error message saying lake is an unknown command and you have not logged in since you installed Lean, then you may need to first type 
# source ~/.profile or source ~/.bash_profile
# - Go inside the my_project folder and type lake update, then lake exe cache get and then mkdir MyProject.
cd my_project
lake update 
lake exe cache get
mkdir MyProject
# Your Lean code should now be put inside files with extension .lean living in my_project/MyProject/ or a subfolder thereof.
cd MyProject
echo 'import Mathlib.Topology.Basic\n\n#check TopologicalSpace' > Test.lean

You will likely also have to go to the lean_src_proj and rm -rf .git if you want to git push the lean project code. For some reason lake create a git repo for you.