1
$\begingroup$

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'

enter image description here


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.

$\endgroup$
6
  • $\begingroup$ Your project is in my_project not in MyProject. $\endgroup$ Feb 23 at 2:48
  • $\begingroup$ Also, it's probably not a good idea to force an old Lean version, 2023-02-04 is over a year old! $\endgroup$ Feb 23 at 5:48
  • $\begingroup$ @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 leanprover-community.github.io/install/… so idk, I'm just reading them and following what the lean maintainers tell me to do. I agree with you at first glance. $\endgroup$ Feb 23 at 20:16
  • $\begingroup$ @FrançoisG.Dorais my understanding is that there are 3 folders (very confusing). The first folder is the root (for me $HOME in the example that actually works) where the lean project will be called my_project in my example. That folder will have a bunch of lean files like .lake, lakefile.lean, lean-toolchain etc. Then inside my_folder there will be the folder where the actual lean src code will be. That is the third folder called MyProject. This is the structure if I understand the official instructions correctly $\endgroup$ Feb 23 at 20:19
  • $\begingroup$ official instructions I am following leanprover-community.github.io/install/… and details in question of exact commands I ran in my local mac computer $\endgroup$ Feb 23 at 20:20

2 Answers 2

3
$\begingroup$

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:

enter image description here

$\endgroup$
9
  • $\begingroup$ Mysterious. I'm not opening vscode from the terminal. I'm just clicking the icon and then creating a workspace by adding the root folder. Is there a solution where it doesn't require me to open vscode from some weird directory? e.g., can I tell vscode where the path to lean is or something or my lean "env" just like I'd do with python pointing to a conda env? $\endgroup$ Feb 24 at 23:19
  • $\begingroup$ what is this the system config files for the project? Can I edit this? $\endgroup$ Feb 24 at 23:20
  • $\begingroup$ note, this answer also complicates my workflow because I will be using the ssh extension of vscode (and I can't do code $HOME/proj_path since there isn't vscode in the remote servers) and developing lean in remote servers. So I think it's needed for me to know precisely what the issue is so I can decide what the solution is besides locally opening the lean project that way. I'd like to be able to see all my lean, python, bash etc file in the root of my directory structure and have vscode's lean work properly. Btw, thanks for the help! $\endgroup$ Feb 24 at 23:24
  • 1
    $\begingroup$ 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. $\endgroup$ Feb 25 at 1:13
  • $\begingroup$ thank you Kevin! Definitively tried **Click the icon and then use "file" -> "open folder" and open the project folder, not the root folder. ** but I think I needed to restart vscode. I think vscode might get confused if there is already a Lean server running and at the same time from vscode's integrated terminal I start trying to set up a project. Not sure how exactly the vscode knows "where Lean is" and the respective "lean environments" but for now restarting and opening as you suggested worked. If you know where to read about the above question it would be appreciated! (I come from python) $\endgroup$ Feb 27 at 18:29
0
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ say that I git clone my project. So it pulls my_project. However, if I run lake +leanprover/lean4:nightly-2023-02-04 new my_project math it complains that my_project already exists. How do I make sure to setup matlib again for my_project in this case? $\endgroup$ Feb 27 at 19:04
  • $\begingroup$ I also noticed I have to cd lean_src_proj and rm -rf .git for me to push the code from lean there. $\endgroup$ Feb 28 at 18:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.