unknown package in lean4-samples

Stream: lean4

[Thomas Eckl]

I would like to play around with Lean 4, so I installed the system and copied the lean4-samples from GitHub. The HelloWorld example works fine, but when loading Main.leanof the CSVParser example, the following error message appears in Lean Infoview:

unknown package 'CSVParser'
You might need to open '...' as a workspace in your editor

Since the import of Lean.Data.Parsec in CSVParser.lean works fine, I guess that it's not a problem with the general setup, but a missing path somewhere. But how and where to add it? As a path variable? In lakefile.lean?
Strangely enough lake build worked without error message. But I am not sure how to test its output.

[Sebastian Ullrich]

Did you open the CSVParser directory as a workspace ("Open Folder..." in VS Code) as suggested in the error message?

[Thomas Eckl]

Worked! And I have missed this instruction in the Lean 4 Manual - sorry.

[Sebastian Ullrich]

Is there anything we can clarify in the message or manual?

[Thomas Eckl]

It's more that VS Code is misleading, because there is no option Open Workspace ... in the File menu. The instruction in the manual is obvious, once you read it.

[Thomas Eckl]

Next problem: I want to create a Lean package using lake init Test and then lake build to get an executable version. The following error messages appear:

error: .\lakefile.lean:1:0: error: unknown package 'Init'
error: .\lakefile.lean:2:0: error: unknown namespace 'Lake'
error: .\lakefile.lean:4:0: error: expected command
error: .\lakefile.lean:13:0: error: expected 'abbrev', 'axiom', 'builtin_initialize', 'class', 'def', 'example', 'inductive', 'initialize', 'instance', 'opaque', 'structure', 'syntax' or 'theorem'
error: .\lakefile.lean: package configuration has errors

lakefile.lean produces the error message unknown package 'Init' in the first line import Lake.

[Thomas Eckl]

elan self update yields

←[1minfo: ←[0mchecking for self-updates
←[31m←[1merror: ←[0mcould not create link from 'C:\Users\Thomas\.elan\bin\elan.exe' to 'C:\Users\Thomas\.elan\bin\lake.exe'

[Sebastian Ullrich]

This could mean that there is still a lake.exe running

[Thomas Eckl]

I couldn't see a lake in the task manager, and a restart of windows also didn't change the message.

[Thomas Eckl]

The Test.lean file yields the error message

`c:\Users\Thomas\.elan\toolchains\leanprover--lean4---nightly-2022-08-12\bin\lake.exe print-paths Init` failed:

[Thomas Eckl]

Is it a problem that there are different versions of lake around, one in C:\Users\Thomas\.elan\bin\lake.exe, one in C:\Users\Thomas\.elan\toolchains\leanprover--lean4---nightly-2022-08-12\bin?

[Sebastian Ullrich]

No, that's as expected. Unfortunately I'm not sure what else to say, I've never seen this error before, and I don't use Windows myself.

[Thomas Eckl]

I changed the lean-toolchain from leanprover/lean4:nightly-2022-08-12 to leanprover/lean4:nightly, and then the error messages for the Llean-files in the Test-folder disappear, and lake build works.

[Sebastian Ullrich]

What does lean --version report now? If it's newer, then I suppose we're good.

[Thomas Eckl]

Lean (version 4.0.0-nightly-2022-08-12, commit 104196e599b3, Release) - seems not to have changed.

[Sebastian Ullrich]

Wow, okay...

[Thomas Eckl]

When I try to update lean with elan default leanprover/lean4:nightly I always get the message

←[1minfo: ←[0musing existing install for 'leanprover/lean4:nightly'
←[1minfo: ←[0mdefault toolchain set to 'leanprover/lean4:nightly'

  ←[1mleanprover/lean4:nightly unchanged←[0m - Lean (version 4.0.0-nightly-2022-08-12, commit 104196e599b3, Release)

[Sebastian Ullrich]

default doesn't update, update does

[Thomas Eckl]

The elan version is elan 1.4.1 (6a7f30d8e 2022-04-15)

[Thomas Eckl]

elan update leanprover/lean4:nightly indeed updated lean, and the test files work fine! :smile:

[Chris Lovett]

Regarding the top of this thread, I added the following missing info to the top level readme.me in the lean4-samples:

Then you need to open each sample folder separately in VS Code using the File->Open folder... menu.

Note: there are no "workspace" samples yet. but there is one checked into vscode-lean4.