Import file from same directory

Stream: new members

[Vivek Rajesh Joshi]

I'm working in ge_test.lean and I want to import ReducedEchelon.lean into it. How do I do it?
image.png

[Anand Rao Tadipatri]

import GaussElim.ReducedEchelon at the top of the file should work.

[Vivek Rajesh Joshi]

This is the error it gives:
unknown package 'GaussElim' You might need to open 'c:\...\gauss_elim' as a workspace in your editor

[Anand Rao Tadipatri]

It looks like the name of the project might be MyProject. Could you share the contents of your lakefile?

I suspect that changing the folder name from GaussElim to MyProject and then importing MyProject.ReducedEchelon will solve the issue.

[Vivek Rajesh Joshi]

Yes, I think that's the case
Contents of lakefile:

import Lake
open Lake DSL

package «my_project» where
  -- Settings applied to both builds and interactive editing
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
  ]
  -- add any additional package configuration options here

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_lib «MyProject» where
  -- add any library configuration options here

[Vivek Rajesh Joshi]

Would it work if I changed MyProject here to GaussElim?

[Anand Rao Tadipatri]

Yes, I think it would. You may need to re-open the project after updating the lakefile.

[Vivek Rajesh Joshi]

Nope, still the same problem

[Anand Rao Tadipatri]

How about creating a new Lean project with the name GaussElim and either moving all files there or copying the configuration files over to your existing repository? If I remember correctly, there also needs to be top-level file with the name GaussElim.lean.

[Vivek Rajesh Joshi]

Ohh okay, I'll try it out

[Paul Schwahn]

I had a very similar problem here, which Kevin helped me with.

As far as I understand it now, there is a distinction between packages and libraries: The entire project folder corresponds to a package, while libraries inside the package correspond to subfolders. Both the package and its libraries need to be initialized in the lakefile of the package.
(Someone please correct me if I'm wrong!)

[Paul Schwahn]

And then there's the top-level lean file that I still don't understand: does it always have to be the package's name in camel case (my_project -> MyProject)? And what is actually its purpose?