Zulip Chat Archive

Stream: lean4

Topic: unknown package in lean4-samples


Thomas Eckl (Aug 30 2022 at 09:04):

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 (Aug 30 2022 at 09:09):

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

Thomas Eckl (Aug 30 2022 at 09:19):

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

Sebastian Ullrich (Aug 30 2022 at 09:20):

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

Thomas Eckl (Aug 30 2022 at 09:24):

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 (Aug 30 2022 at 10:42):

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 (Aug 30 2022 at 12:42):

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 (Aug 30 2022 at 12:44):

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

Thomas Eckl (Aug 30 2022 at 14:18):

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

Thomas Eckl (Aug 30 2022 at 14:23):

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 (Aug 30 2022 at 15:03):

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 (Aug 30 2022 at 15:04):

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 (Aug 30 2022 at 15:28):

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 (Aug 30 2022 at 15:29):

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

Thomas Eckl (Aug 30 2022 at 15:30):

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

Sebastian Ullrich (Aug 30 2022 at 15:31):

Wow, okay...

Thomas Eckl (Aug 30 2022 at 15:33):

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 (Aug 30 2022 at 15:35):

default doesn't update, update does

Thomas Eckl (Aug 30 2022 at 15:49):

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

Thomas Eckl (Aug 30 2022 at 16:00):

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

Chris Lovett (Aug 31 2022 at 03:21):

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.


Last updated: Dec 20 2023 at 11:08 UTC