Search path for packages?

Stream: new members

[Martin C. Martin]

In my project, I have a src directory, then a mypackage directory, which has two files A.lean and B.lean. However, at the start of B.lean, when I try import mypackage.A, I get the error unknown package 'mypackage'.

Is there documentation somewhere of how to add the src directory to the search path? I would have thought it was added by default. Thanks.

[Yaël Dillies]

See the readme of the lake repo.

[Shreyas Srinivas]

You are missing a mypackage.lean file which is at the same level as the mypackage folder in the directory hierarchy

[Shreyas Srinivas]

You will also need an src.lean file at the same level of src .

[Martin C. Martin]

Is the canonical setup not to have a src directory, and just put the mypackage directory in the root, next to lakefile.lean, lean-toolchain, etc?

[Shreyas Srinivas]

Yes

[Shreyas Srinivas]

The build folder is already separate

[Shreyas Srinivas]

See the standard template that lake generates for you when you use lake new

[Shreyas Srinivas]

You will find a <project_name>.lean file and a <project_name>/Basic.lean file

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

If you want a separate test directory, you can add a Tests.lean file and a corresponding Tests/ folder

[Shreyas Srinivas]

(deleted)