Zulip Chat Archive

Stream: new members

Topic: Lake creates lean3 project structure


Twm Stone (Dec 22 2024 at 09:08):

I'm looking at https://lean-lang.org/functional_programming_in_lean/hello-world/starting-a-project.html and attempting to start a new project, having installed lean4 / lake5. When I create a new project it sets up a lakefile.toml rather than a lakefile.lean which I think means it's getting confused?

tops@TOPS:~$ lake --version
Lake version 5.0.0-410fab7 (Lean version 4.14.0)
tops@TOPS:~$ lean --version
Lean (version 4.14.0, x86_64-unknown-linux-gnu, commit 410fab728470, Release)

Kyle Miller (Dec 22 2024 at 09:12):

lakefile.toml is the new default for projects

Kyle Miller (Dec 22 2024 at 09:14):

lean4#5504

Twm Stone (Dec 22 2024 at 09:14):

oh so the textbook is just out of date?

Twm Stone (Dec 22 2024 at 09:15):

I originally was looking into this because having created a new project I get the error

unknown module prefix 'Py2lean'

No directory 'Py2lean' or file 'Py2lean.olean' in the search path entries:
/home/tops/.elan/toolchains/stable/lib/lean

Twm Stone (Dec 22 2024 at 09:16):

and I assumed that the absolute minimal project lake would create wouldn't have errors in it

Kyle Miller (Dec 22 2024 at 09:19):

Where are you getting this error?

Twm Stone (Dec 22 2024 at 09:20):

the tool has created a Main.lean which looks like this:

import Py2lean

def main : IO Unit :=
  IO.println s!"Hello, {hello}!"

I've opened it in VSCode and the import statement is marked as an error in the Lean Infoview

Kyle Miller (Dec 22 2024 at 09:21):

How did you open it in VSCode? Did you open the project folder?

Twm Stone (Dec 22 2024 at 09:21):

yes

Kyle Miller (Dec 22 2024 at 09:22):

If you do lake build from within the root of the project on the command line, do you get an error?

Twm Stone (Dec 22 2024 at 09:23):

tops@TOPS:~/py2lean$ lake build
info: py2lean: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
 [2/5] Running py2lean
error: ././././Main.lean: bad import 'Py2lean'
 [3/5] Running Py2lean
error: no such file or directory (error code: 2)
  file: ././././Py2lean.lean
 [4/5] Running Main
error: ././././Main.lean: bad import 'Py2lean'
Some required builds logged failures:
- py2lean
- Py2lean
- Main
error: build failed```

Kyle Miller (Dec 22 2024 at 09:23):

(And be sure to double check you've opened the folder containing the lakefile. This is a common mistake when getting started.)

Twm Stone (Dec 22 2024 at 09:23):

tops@TOPS:~/py2lean$ ls -la total 44 drwxr-xr-x 5 tops tops 4096 Dec 22 09:22 . drwxr-x--- 16 tops tops 4096 Dec 22 09:22 .. drwxr-xr-x 7 tops tops 4096 Dec 22 09:22 .git drwxr-xr-x 3 tops tops 4096 Dec 22 09:14 .github -rw-r--r-- 1 tops tops 7 Dec 22 09:14 .gitignore -rw-r--r-- 1 tops tops 71 Dec 22 09:14 Main.lean drwxr-xr-x 2 tops tops 4096 Dec 22 09:14 Py2lean -rw-r--r-- 1 tops tops 9 Dec 22 09:14 README.md -rw-r--r-- 1 tops tops 113 Dec 22 09:22 lake-manifest.json -rw-r--r-- 1 tops tops 140 Dec 22 09:14 lakefile.toml -rw-r--r-- 1 tops tops 7 Dec 22 09:14 lean-toolchain

Kyle Miller (Dec 22 2024 at 09:24):

What's the contents of the lakefile?

I'm wondering if there's a case sensitivity issue.

Twm Stone (Dec 22 2024 at 09:25):

ooh, maybe

tops@TOPS:~/py2lean$ cat lakefile.toml
name = "py2lean"
version = "0.1.0"
defaultTargets = ["py2lean"]

[[lean_lib]]
name = "Py2lean"

[[lean_exe]]
name = "py2lean"
root = "Main"```

Kyle Miller (Dec 22 2024 at 09:27):

I'm looking at your directory listing again, and where's the Py2lean.lean file?

Kyle Miller (Dec 22 2024 at 09:27):

I just did lake new Py2lean and lake new py2lean to check, and in both cases there's a Py2lean.lean file

Kyle Miller (Dec 22 2024 at 09:28):

I'm using the exact same version of lake as you are

Twm Stone (Dec 22 2024 at 09:29):

doesn't look like I have one

Twm Stone (Dec 22 2024 at 09:29):

I'm running on WSL / Ubuntu, in case that makes any difference

Kyle Miller (Dec 22 2024 at 09:30):

What's the exact lake new command you ran?

Twm Stone (Dec 22 2024 at 09:31):

looking at my bash history, it existed before I ran the build command ??

Twm Stone (Dec 22 2024 at 09:31):

I'll recreate py2lean

Twm Stone (Dec 22 2024 at 09:33):

ok wtf that now builds

Twm Stone (Dec 22 2024 at 09:34):

thanks for your help, I think that should just be fine now, apparently

Kyle Miller (Dec 22 2024 at 09:35):

What a mystery, glad you're not stuck on build systems now

Mauricio Collares (Dec 22 2024 at 10:09):

Twm Stone said:

oh so the textbook is just out of date?

If you're following Functional Programming in Lean, the best way to have a smooth experience is to use the Lean version it was tested on, which is 4.1.0. If you use a newer version of Lean, you will encounter a few minor issues. To use Lean 4.1.0, you can create the project with lake +leanprover/lean4:v4.1.0 new greeting. You don't need to include the +leanprover/lean4:v4.1.0 part in other Lake commands. See #general > ✔ Error in proof example from Functional Programming book? @ 💬 for an in-depth discussion by the author.

(Don't get discouraged by that, the book is great and almost all you learn there will transfer to newer Lean versions! The changes were minor. You can also proceed with your current version and ask further questions here if some sample does not work. If you're not following the book closely, then using the most recent Lean version is probably better, as there have been multiple usability improvements.)


Last updated: May 02 2025 at 03:31 UTC