Problem with Imports

Stream: new members

[Colin ⚛️]

Is there anyway to fix this issue?

Error Message:

stderr:
✖ [2/3] Running LeanGenetics.Basic
error: no such file or directory (error code: 2)
  file: C:\Users\Colin\LeanGenetics\LeanGenetics\Basic.lean
✖ [3/3] Running setup (LeanGenetics)
error: C:\Users\Colin\LeanGenetics\LeanGenetics.lean: bad import 'LeanGenetics.Basic'
Some required builds logged failures:
- LeanGenetics.Basic
- setup (LeanGenetics)
error: build failed

From the code in the .lean files, in this example LeanGenetics.lean

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

import «LeanGenetics».Basic

This happens whenever I create a new project and follow the steps here under "Creating a New Lean Project".

[Colin ⚛️]

Here is what my directory looks like:
Screenshot 2025-09-02 211023.png

[Colin ⚛️]

It might be out of date, but I've had this problem with other projects where the imports don't work even after updating.

[Niels Voss]

Sorry if you've already tried this, but it seems to me that your code wants to import LeanGenetics.Basic, but that file doesn't exist (and presumably GeneticCode.Basic exists instead?)

[Niels Voss]

Oh I think I see the issue. You are trying to import the "Basic.lean" file in your current directory. But when you tell Lean to import LeanGenetics.Basic, it instead searches for it in the LeanGenetics folder (which doesn't exist). To fix this, you need to move your Basic.lean file into a LeanGenetics folder

[Niels Voss]

Alternatively, you could just import Basic instead of import LeanGenetics.Basic (although in the long run, that's probably a bad decision since it requires declaring stuff at top level)

[Colin ⚛️]

LeanGenetics does exist though. I should have shown more of my directory. Here's the full screenshot.
Screenshot 2025-09-09 141911.png

[Colin ⚛️]

Doing this in LeanGenetics.lean doesn't work either even though the file "GeneticCode.lean" exists definitely in the file GeneticCode shown in the screenshot above.

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

[Colin ⚛️]

It gives a rather long error message

No directory 'GeneticCode' or file 'GeneticCode.olean' in the search path entries:
C:\Users\Colin\LeanGenetics\.lake\packages\Cli\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\batteries\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\Qq\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\aesop\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\proofwidgets\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\importGraph\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\LeanSearchClient\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\plausible\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\mathlib\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\Cli\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\batteries\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\Qq\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\aesop\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\proofwidgets\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\importGraph\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\LeanSearchClient\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\plausible\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\packages\mathlib\.lake\build\lib\lean
C:\Users\Colin\LeanGenetics\.lake\build\lib\lean
c:\Users\Colin\.elan\toolchains\leanprover--lean4---v4.21.0-rc3\lib\lean
c:\Users\Colin\.elan\toolchains\leanprover--lean4---v4.21.0-rc3\lib\lean

[Colin ⚛️]

Can anyone provide pointers on this?

[Ruben Van de Velde]

How did you create this project? Typically you have an XXX.lean file and an XXX folder at the top of your project

[Matt Diamond]

LeanGenetics does exist though

The issue is that LeanGenetics as a folder within the current folder does not exist. Lean is looking for C:\Users\Colin\LeanGenetics\LeanGenetics\Basic.lean, but that file doesn't exist. You want it to look for C:\Users\Colin\LeanGenetics\Basic.lean.

That being said, I don't know why your second example doesn't work.

[Colin ⚛️]

I made my project using the steps outlined here: https://leanprover-community.github.io/install/project.html

Under Creating New Projects