Creating a new Lean project

Stream: new members

[Matthias U]

I'm quite new to Lean and I tried creating a new Lean project using the instructions given here: https://leanprover-community.github.io/install/project.html .
However, when I open an empty .lean file, VS Code tells me "Server has stopped with Error code 1".
After I copied the files "leanpkg.toml" and "leanpkg.path" from an existing project (e.g. the tutorial project) and ran 'leanpkg configure' and 'leanproject get-mathlib-cache', I could use Lean normally and it is working now.
Still, I was wondering if there is a more elegant way to create a new project, in particular is this possible without copying files from an existing one?

[Riccardo Brasca]

You have to open the folder in VS Code, not the single file.

[Riccardo Brasca]

Then you can create a new file

[Yakov Pechersky]

leanproject new my_project like the directions suggest, then opening my_project (the new directory) using VS Code, not any of the lean files in it. Then once you've opened the directory in VS Code, feel free to make any new lean files in the src directory. This is all pretty much how the steps in the instructions are.

[Matthias U]

Riccardo Brasca said:

You have to open the folder in VS Code, not the single file.

Thanks, I opened the folder but I still get the error

[Matthias U]

Yakov Pechersky said:

leanproject new my_project like the directions suggest, then opening my_project (the new directory) using VS Code, not any of the lean files in it. Then once you've opened the directory in VS Code, feel free to make any new lean files in the src directory. This is all pretty much how the steps in the instructions are.

If I type leanproject new my_project, I get the error uncaught exception: Lean package manager, version 4.0.0 Usage: leanpkg <command>.

[Yakov Pechersky]

Ah, you're trying to work with Lean4. leanproject, mathlib in it's current state, and this channel, are all for Lean3

[Riccardo Brasca]

If you are new to Lean and you don't have any special reason to do otherwise, just go with Lean 3

[Yakov Pechersky]

Unless I misunderstood something. Of course, copying the various config files from the tutorials will make you use Lean3 in the directory through recognition of those files by elan, which is the lean version manager.

[Matthias U]

Actually, I'm trying to work with Lean 3. Does this mean that I have the wrong version of leanproject?

[Riccardo Brasca]

You probably have the wrong version of Lean. Which OS are you using?

[Kevin Buzzard]

Did you follow the installation instructions here ?

[Matthias U]

Yes, I followed the 'fastest way' indicated for Ubuntu. I'm using Ubuntu 20.04

[Riccardo Brasca]

You mean this?

wget -q https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

[Matthias U]

Yes, exactly

[Kevin Buzzard]

So you're opening a folder containing a Lean 3 project in VS Code and you're getting an error?

[Matthias U]

Yes

[Kevin Buzzard]

Can you upload a screenshot of what your VS Code looks like after you've opened the project folder?

[Riccardo Brasca]

Also, what lean -v says? Just to be sure you have lean3...

[Kevin Buzzard]

Riccardo, the output of lean -v will depend on the directory in which it is run

[Kevin Buzzard]

buzzard@bob:~/active-lean-projects$ cd lean-liquid/
buzzard@bob:~/active-lean-projects/lean-liquid$ lean -v
Lean (version 3.30.0, commit a5822ea47ebc, Release)
buzzard@bob:~/active-lean-projects/lean-liquid$ cd ..
buzzard@bob:~/active-lean-projects$ cd lean4-filters/
buzzard@bob:~/active-lean-projects/lean4-filters$ lean -v
Lean (version 4.0.0-nightly-2021-04-29, commit 40b17bc364dd, Release)
buzzard@bob:~/active-lean-projects/lean4-filters$

[Kevin Buzzard]

This is normal

[Matthias U]

Screenshot_2021-05-12_15-54-58.png VS Code looks as follows

[Riccardo Brasca]

Yes, but I think leanproject new will use the Lean installed in the system... but maybe I am wrong

[Matthias U]

lean -v yields Lean (version 4.0.0-m1, commit 34cf4bc3ffc3, Release)

[Kevin Buzzard]

So that is not a correct-looking lean project because it has e.g. no path file. How did you make this project?

[Kevin Buzzard]

Riccardo there is no such thing as "the Lean installed in the system"

[Kevin Buzzard]

leanproject will only make Lean 3 projects

[Matthias U]

I typed into a terminal leanproject new . When I typed leanproject new project_name it told me uncaught exception: Lean package manager, version 4.0.0

[Kevin Buzzard]

OK so right now your problem is that you don't have a valid Lean project to open.

[Kevin Buzzard]

When you say leanproject new do you mean leanproject new without any name at all?

[Matthias U]

Yes, just leanproject new without any name

[Kevin Buzzard]

if I type that in an empty directory it creates a project whose name is the name of the directory I'm in but it creates a path file. I recommend you delete your corrupted project, and type leanproject new my_project in a directory which doesn't contain any leanpkg.path or leanpkg.toml or indeed any file at all. What happens then?

[Matthias U]

I'm getting the following error `
uncaught exception: Lean package manager, version 4.0.0

Usage: leanpkg <command>

configure download and build dependencies and print resulting LEAN_PATH
build [-- <Lean-args>] configure and build *.olean files
init <name> create a Lean package in the current directory

See leanpkg help <command> for more information on a specific command.
Command '['leanpkg', 'new', 'my_project']' returned non-zero exit status 1.`

[Kevin Buzzard]

I think this is what we should fix before going on.

[Kevin Buzzard]

What does leanpkg --help return?

[Matthias U]

`uncaught exception: Lean package manager, version 4.0.0

Usage: leanpkg <command>

configure download and build dependencies and print resulting LEAN_PATH
build [-- <Lean-args>] configure and build *.olean files
init <name> create a Lean package in the current directory

See leanpkg help <command> for more information on a specific command.`

[Kevin Buzzard]

oh sorry, leanpkg help

[Kevin Buzzard]

But this "uncaught exception" doesn't bode well

[Matthias U]

leanpkg help also returns

[Matthias U]

Lean package manager, version 4.0.0

Usage: leanpkg <command>

configure download and build dependencies and print resulting LEAN_PATH
build [-- <Lean-args>] configure and build *.olean files
init <name> create a Lean package in the current directory

See leanpkg help <command> for more information on a specific command.

[Matthias U]

Matthias U said:

leanpkg help also returns

I mean 'returns' (there isn't the uncaught exception)

[Kevin Buzzard]

Is there some leanpkg.toml file in a directory above the directory you are in currently?

[Kevin Buzzard]

I can reproduce this error by putting a Lean 4 leanpkg.toml in a directory above the directory I am currently in.

[Matthias U]

In the current directory, there are no files at all

[Kevin Buzzard]

I am asking about every directory above the directory where you are in, right up to /

[Kevin Buzzard]

If I put a leanpkg.toml which mentions Lean 4 in one of these directories then leanpkg gets confused and assumes you are making a Lean 4 repo, but leanproject expects you to be making a Lean 3 repo, and this gives the errors you are reporting.

[Kevin Buzzard]

So I conjecture that you are making a repo within another repo, or another failed attempt at making a repo, or whatever.

[Matthias U]

Yes, in my home directory, there is one. I'm removing it...

[Kevin Buzzard]

@Patrick Massot you'll love this one

[Kevin Buzzard]

buzzard@bob:~$ mkdir test
buzzard@bob:~$ cd test
buzzard@bob:~/test$ cat > leanpkg.toml
[package]
name = "this_will_mess_up_leanproject"
version = "0.1"
lean_version = "leanprover/lean4:nightly"
buzzard@bob:~/test$ mkdir test2
buzzard@bob:~/test$ cd test2
buzzard@bob:~/test/test2$ leanproject new this_wont_work
uncaught exception: Lean package manager, version nightly-2021-04-29

Usage: leanpkg <command>

init <name>      create a Lean package in the current directory
configure        download and build dependencies
build [<args>]   configure and build *.olean files

See `leanpkg help <command>` for more information on a specific command.
Command '['leanpkg', 'new', 'this_wont_work']' returned non-zero exit status 1.
buzzard@bob:~/test/test2$

[Matthias U]

Ok, I removed all *.lean files, the leanpkg.toml and the .gitfolder from my home directory, but I'm still getting the same error message

[Kevin Buzzard]

Did you check for Lean files all the way from where you are running the command right up until /?

[Yakov Pechersky]

What do the following commands say, when running them from the directory where you ran leanproject new?

elan which lean
elan toolchain list

[Patrick Massot]

When creating a new project, leanproject uses leanpkg which itself uses what elan thinks is the default version of Lean. Clearly Matthias' elan think Lean 4 is the default Lean version, so everything is broken.

[Matthias U]

Yakov Pechersky said:

What do the following commands say, when running them from the directory where you ran leanproject new?

elan which lean
elan toolchain list

I get the following paths `/home/matthias/.elan/toolchains/leanprover-lean4-stable/bin/lean'

[Matthias U]

and stable leanprover-community-lean-3.27.0 leanprover-community-lean-3.28.0 leanprover-lean4-stable (default)

[Matthias U]

I just fixed the problem! In case you're interested: I uninstalled elan via elan self uninstall and reran the installation of lean. Now elan which lean just yields stable

[Matthias U]

Also then leanproject new my_projectworks and installs mathlib without problems and I can use Lean normally afterwards.

[Matthias U]

Thank you very much for your help!