leanpkg now expects sources in src/ subdirectory, but doesn't look for them there in dependent projects.

[kim-em]

leanpkg was recently modified so leanpkg build runs lean --make src, so I've moved all my sources into src/ subdirectories. However now when a second project has a dependency on a first project, it can't find any of the files, because they're now all in the src/ subdirectory.

Hopefully this makes sense without a minimal example; let me know if I should add one.

[jroesch]

Are you putting all of your files directly in the source directory? the intended design is similar to Java, you should place lean files in src/pkg_name/default.lean so that you are able to do import pkg_name in packages which depend on it. My change was only to make src the default path, you can also set path explicitly in your leanpkg.toml file, path = "my_src_path".

Using the package directory as the path for --make is problematic as it means leanpkg build will fail if any other lean file fails, for example a test file in test.

[jroesch]

For example I am able to import smt2_interface in a project with this TOML:

[package]
name = "my_awesome_pkg"
version = "0.1"
path = "src"

[dependencies]
smt2_interface = { path = "/Users/jroesch/Git/smt2_interface" }

My code resides in smt_interface/src/smt2 and I am able to do import smt2.

[gebner]

@semorrison Sorry, I completely overlooked this change in PR #1599. I have reverted it now. The sources are supposed to be in whatever directory the path attribute specifies, it defaults to ..

@jroesch If you want to change the default source directory, then please make a separate PR. You need to change manifest.effective_path as well, which returns the source directories for a package. Otherwise, import resolution will not work across packages as @semorrison observed. Besides, I think we need to make this change a bit more gradually--introduce a warning now that the default will change, then change the default and print a warning that there's a new default, and later remove the warnings.

[kim-em]

Can someone help me understand how to make the imports work in my two projects?

They are at https://github.com/semorrison/lean-category-theory and https://github.com/semorrison/lean-monoidal-categories.

The lean-monoidal-categories repository has the following leanpkg.toml file:

[package]
name = "monoidal-categories"
version = "0.1"

[dependencies]
lean-category-theory = { git = "https://github.com/semorrison/lean-category-theory", rev = "977d9df11e19673b9299d20f44cd602eb652898c" }

The directory structures look like

src/
  category_theory/
     categories.lean
     products/
       associator.lean

and

src/
  monoidal_categories/
    tensor_products.lean

(and of course many other files).

In thelean-monoidal-categories repository, the file src/monoidal_categories/tensor_products.lean begins with import category_theory.products.associator, but running leanpkg build reports:

/Users/scott/projects/lean-monoidal-categories/src/monoidal_categories/tensor_product.lean:1:0: error: file 'category_theory/products/associator' not found in the LEAN_PATH

From what I understand of the above, this is what I'm meant to be doing.... :-(

[kim-em]

Ah scratch that, I've read @gebner's comment properly now, and see that the problematic change was reverted. Nevertheless I've switched to putting everything in the src/ subdirectory, and set path = src explicitly in leanpkg.toml, and it seems everything works nicely now.

Thanks everyone!