Problems with import

Stream: lean4

[Hannah Santos]

Hello, I've been trying to make a lean project since earlier, and I was testing if the imports worked properly, I've not done this before, so I'm not sure what the problem is, can anyone help me, please?
Import_not_working
(I wasn't sure how to post this, because the problem is not the code, so I didn't think the usual way would've helped? Since it would need both files and everything, I can provide whatever as needed)

[Hannah Santos]

If anyone needs the output:

/-/-/Lean/Lean_Presentation/Examples> curl --version
curl 7.74.0 (x86_64-pc-linux-gnu) libcurl/7.74.0 OpenSSL/1.1.1n zlib/1.2.11 brotli/1.0.9 libidn2/2.3.0 libpsl/0.21.0 (+libidn2/2.3.0) libssh2/1.9.0 nghttp2/1.43.0 librtmp/2.3
Release-Date: 2020-12-09
Protocols: dict file ftp ftps gopher http https imap imaps ldap ldaps mqtt pop3 pop3s rtmp rtsp scp sftp smb smbs smtp smtps telnet tftp
Features: alt-svc AsynchDNS brotli GSS-API HTTP2 HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM NTLM_WB PSL SPNEGO SSL TLS-SRP UnixSockets

/-/-/Lean/Lean_Presentation/Examples> git --version
git version 2.30.2

/-/-/Lean/Lean_Presentation/Examples> lean --version
Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)
/-/-a/Lean/Lean_Presentation/Examples> elan --version
elan 3.1.1 (71ddc6633 2024-02-22)

/-/-/Lean/Lean_Presentation/Examples> lean --version
Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)
/-/-/Lean/Lean_Presentation/Examples> lake --version
Lake version 5.0.0-6fce8f7 (Lean version 4.7.0)

[Kevin Buzzard]

Try moving all your files into the Examples directory and importing things like Examples.Example_Prop. The first "word" of the import needs to be the name of the package that the file lives in (like import Mathlib.Tactic). If this doesn't work, post your lakefile.lean so we can see the name of your package.

[Hannah Santos]

This one?

import Lake
open Lake DSL

package «Examples» where
  -- add package configuration options here

lean_lib «Examples» where
  -- add library configuration options here

@[default_target]
lean_exe «examples» where
  root := `Main

[Hannah Santos]

It's still saying this:

object file './.lake/build/lib/Examples/Example_Prop.olean' of module Examples.Example_Prop does not existLean 4
`/home/sibylla_a/.elan/toolchains/leanprover--lean4---stable/bin/lake setup-file /home/sibylla_a/Lean/Lean_Presentation/Examples/Examples/Example_Complexity.lean Init Examples.Example_Prop --no-build` failed:

stderr:
error: 'Examples.Example_Prop': no such file or directory (error code: 2)
  file: ./././Examples/Example_Prop.lean
Lean 4
processing stopped

[Kevin Buzzard]

Right! You've made a package called Examples which means that all your local imports should look like import Examples.foo which means that they should all be in the directory called Examples, just like the file Tactic.lean is in the directory Mathlib of the Mathlib repo.

[Kevin Buzzard]

Did you move the file into the directory yet?

[Hannah Santos]

Yes.

[Kevin Buzzard]

hmm! Maybe restart Lean and/or VS Code?

[Hannah Santos]

I'll try.

[Hannah Santos]

Okay, it seems restarting it makes it understand and process it, but now there's this problem that wasn't one before, on main.lean:
lean

[Hannah Santos]

Do all of the files, even the lake ones should be inside the Examples folder?

[Hannah Santos]

(Just trying to make sure)

[Hannah Santos]

Well, somehow, it worked.

[Hannah Santos]

Had to organize it like this

[Hannah Santos]

Thank you!

[Kevin Buzzard]

Definitely .lake should be in the root of the project, not in Examples. See a project like mathlib to see what it should look like. All the lean files are in the directory Mathlib apart from Mathlib.lean, and all the other files aren't.

[Hannah Santos]

So.... In my case it's kind of repeated?

[Kevin Buzzard]

In fact you have two .lake directories, maybe just delete the one in Examples?

[Hannah Santos]

Okay!

[Hannah Santos]

It's working, thank you.

[Hannah Santos]

(Tried with another project to see if it was fine, so yay!)