Open semorrison opened 2 months ago
I think one confounding issue here is that, like Python it is not necessarily ideal to have users importing their whole package into a top-level module. Ideally, downstream users are expected to import parts of packages piecemeal as needed, not just import a catch-all root.
It seems only option 1 comes without extra code and complexity?
I find it a natural default, more sophisticated libraries can change that.
@tydeu, I think you're making the mistake of optimizing for expert users / complicated projects, rather than for beginners / small projects here. The confounding issue you point out is real, but I don't think warrants not improving life for everyone else.
@semorrison While I do agree that I (probably mistakenly) lean towards experts, my concern here was one focused on beginners. We do not want to habituate them into catch-all roots. However, the globs idea should work for both here.
A pretty common user error in a project
Foo
is to neither modifyFoo.lean
to import their "interesting" files e.g.Foo/XYZ.lean
nor to useglobs := #[.submodules `Foo]
in theirlean_lib
(which, as far as I'm aware, is only discoverable by asking on zulip).They just leave
Foo.lean
with its default contents, and get to work in theFoo
directory, relying on VSCode to show them errors when they open files.This has the effect that
lake build
is essentially a no-op.This is sufficiently common that I think we need to do something about it. It's good that the default template now has a
but I think this isn't enough.
Possible solutions:
lakefile.lean
to use globs, e.g. something like:Foo.lean
only containsimport Foo.Basic
, there is no globs setting, but there are other lean files underFoo/
), and if so give them explanatory text or a warning.Foo.lean
(lake update-imports
??), and warns when it is out of sync, with an option to silence the warning for experts.(I prefer 1. over 2. over 3.)