Lake creates lean3 project structure

Stream: new members

[Twm Stone]

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]

lakefile.toml is the new default for projects

[Kyle Miller]

lean4#5504

[Twm Stone]

oh so the textbook is just out of date?

[Twm Stone]

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]

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

[Kyle Miller]

Where are you getting this error?

[Twm Stone]

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]

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

[Twm Stone]

yes

[Kyle Miller]

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

[Twm Stone]

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]

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

[Twm Stone]

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]

What's the contents of the lakefile?

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

[Twm Stone]

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]

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

[Kyle Miller]

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

[Kyle Miller]

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

[Twm Stone]

doesn't look like I have one

[Twm Stone]

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

[Kyle Miller]

What's the exact lake new command you ran?

[Twm Stone]

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

[Twm Stone]

I'll recreate py2lean

[Twm Stone]

ok wtf that now builds

[Twm Stone]

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

[Kyle Miller]

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

[Mauricio Collares]

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.)