Importing one file into another

Stream: new members

[Martin Epstein]

I'm playing around with a custom binary tree type in a file called "BiTree.lean". I need to use a queue to traverse a BiTree in breadth-first order, so I defined a custom queue type in "Queue.lean". Naturally I put import Queue at the top of "BiTree.lean" but Lean says:

"No directory 'Queue' or file 'Queue.olean' in the search path entries:".

The search path entries are a bunch of .lake and .elan directories so I tried running lake build in the terminal, but this had no effect. My project directory looks like this:

my_lean/
| .git/
| .github/
| .lake/
| src/
. | BiTree.lean
. | Queue.lean
| .gitignore
| lakefile.toml
| lake-manifest.json
| lean-toolchain
| README.md

How can I get import Queue to work?

[Aaron Liu]

How did you set up the Lean project?

[Aaron Liu]

can you list out those search path enteries

[Martin Epstein]

Hi Aaron, I set up the project by selecting "Create Project Using Mathlib..." from the Lean 4 dropdown menu in VS Code. The search path entries are

C:\Users\martin\Code\Lean\my_lean\.lake\packages\Cli\.lake\build\lib\lean
C:\Users\martin\Code\Lean\my_lean\.lake\packages\batteries\.lake\build\lib\lean
C:\Users\martin\Code\Lean\my_lean\.lake\packages\Qq\.lake\build\lib\lean
C:\Users\martin\Code\Lean\my_lean\.lake\packages\aesop\.lake\build\lib\lean
C:\Users\martin\Code\Lean\my_lean\.lake\packages\proofwidgets\.lake\build\lib\lean
C:\Users\martin\Code\Lean\my_lean\.lake\packages\importGraph\.lake\build\lib\lean
C:\Users\martin\Code\Lean\my_lean\.lake\packages\LeanSearchClient\.lake\build\lib\lean
C:\Users\martin\Code\Lean\my_lean\.lake\packages\plausible\.lake\build\lib\lean
C:\Users\martin\Code\Lean\my_lean\.lake\packages\mathlib\.lake\build\lib\lean
C:\Users\martin\Code\Lean\my_lean\.lake\build\lib\lean
c:\Users\martin\.elan\toolchains\leanprover--lean4---v4.24.0-rc1\lib\lean
c:\Users\martin\.elan\toolchains\leanprover--lean4---v4.24.0-rc1\lib\lean

[Aaron Liu]

What's in your lakefile?

[Martin Epstein]

lakefile:

---

name = "my_lean"

version = "0.1.0"

keywords = ["math"]

defaultTargets = ["MyLean"]

[leanOptions]

pp.unicode.fun = true # pretty-prints fun a ↦ b

autoImplicit = false

relaxedAutoImplicit = false

weak.linter.mathlibStandardSet = true

maxSynthPendingDepth = 3

[[require]]

name = "mathlib"

scope = "leanprover-community"

[[lean_lib]]

name = "MyLean"

[Martin Epstein]

By the way, I realized I may have deleted something important. I just created a test standalone project called "foo". It comes with a file "Foo.lean" that says:

-- This module serves as the root of the `Foo` library.
-- Import modules here that should be built as part of the library.

import Foo.Basic

I may have deleted the corresponding file for the project "my_lean". If I create files "bar.lean" and "baz.lean" in the "foo" project then I can import "bar.lean" into "baz.lean" as long as I also import "bar.lean" into "Foo.lean". However, when I tried to imitate this in the "my_lean" project it didn't work.

[Aaron Liu]

Try instead maybe import MyLean.Queue

[Aaron Liu]

Try instead maybe import MyLean.Queue

[Aaron Liu]

or my other guess would be import src.Queue

[Martin Epstein]

Alright, that worked! I had tried import MyLean.Queue and import src.Queue before with no luck, but combined with the steps I mentioned previously this has resolved the issue.