import error

Stream: lean4

[Yakir Mauda]

.

[Yakir Mauda]

.

[Ruben Van de Velde]

Please don't double post, and don't post in random unrelated topics.

[Ruben Van de Velde]

Please don't double post, and don't post in random unrelated topics.

[Yakir Mauda]

Hi everyone!

I'm trying to import system-related modules in my Main.lean file like this:
import System import IO

However, I get the following error:

unknown module prefix 'System' No directory 'System' or file 'System.olean' in the search path entries: .\.\.lake\build\lib .\.\.lake\build\lib c:\Users\user\.elan\toolchains\leanprover--lean4---v4.17.0\lib\lean c:\Users\user\.elan\toolchains\leanprover--lean4---v4.17.0\lib\lean

I don't understand what the problem is or how to solve it.
Could someone please help me? Thanks in advance! :folded_hands:

[Eric Wieser]

Should the error message be improved here? I think this would be clearer as:

No module found for `System`, as `System.olean` could not be found in the search path entries:

[Eric Wieser]

(the error here is that there is no System module)

[Yakir Mauda]

Eric Wieser said:

(the error here is that there is no System module)

Do you know how I can solve this problem?

[Eric Wieser]

Delete the two import lines you wrote, and then tell us what the new error is!

[Yakir Mauda]

Eric Wieser said:

Delete the two import lines you wrote, and then tell us what the new error is!

image.png
too many :/

[Notification Bot]

2 messages were moved here from #general > "Missing Tactics" list by Eric Wieser.

[Mario Carneiro]

it's easier to see lean errors using the infoview BTW, see "Lean 4: Infoview: Toggle Infoview" in the command palette

[Notification Bot]

2 messages were moved here from #Is there code for X? > Fundamental group of the sphere by Eric Wieser.

[Yakir Mauda]

Mario Carneiro said:

Lean 4: Show Infoview

[Mario Carneiro]

You should paste the code here rather than taking screenshots as well. See: #mwe

[Eric Wieser]

The first of these errors is due to missing parentheses, the rest are you trying to call functions that don't exist

[Eric Wieser]

Where did you get this code from? It's quite unusual to write this much code without seeing and fixing the errors as you wrote it.

[Mario Carneiro]

I think we know one source that produces lots of code without typechecking it...

[Yakir Mauda]

Eric Wieser said:

Where did you get this code from? It's quite unusual to write this much code without seeing and fixing the errors as you wrote it.

Sorry in advance, but I uploaded the language book to CHAT-GPT and asked it to help me write a long program.
I don't know the language at all and am having trouble finding an organized way to learn it.

[Ruben Van de Velde]

We strongly recommend not using any kind of LLM to learn lean. There's a number of learning materials listed on the website

[Yakir Mauda]

If I want to tinker with a program that reads and writes to files, what guides are recommended?

[Derek Rhodes]

@Yakir Mauda, For general programming, this is a good starter book:
https://lean-lang.org/functional_programming_in_lean/

There are more books listed here:
https://leanprover-community.github.io/learn.html

Check out this link to get an idea of the package situation:
https://reservoir.lean-lang.org/packages

[Derek Rhodes]

Also, this is a good intro video for just getting started.
https://www.youtube.com/watch?v=FPiykrdPe6U