lean_lib in subdirectory?

Stream: lean4

[Scott Morrison]

@Mac, I was wondering if you could advise on putting a lean_lib in a subdirectory. Mathlib is on its way to acquiring various little "utility" subprojects (many of which will later be upstreamed or moved to separate repositories, but our monorepo tendencies mean they will probably start off incubating in the main repo). We already have cache, and there's a PR for graph (replacing leanproject import-graph).

I'd like to try putting these all in a Util directory.

lean_lib Cache where
  moreLeanArgs := moreLeanArgs
  roots := #[`Util.Cache]

lean_exe cache where
  root := `Util.Cache.Main

is allowed, but only if I then replace all the import Cache.X with import Util.Cache.X.

Is is possibly to organise these utility libraries into a subdirectory, but without changing their module names?

(Saying that this is a terrible idea is also okay --- but then it would nice to have an alternative solution to these cluttering up the root directory, while staying within Mathlib.)

[Yury G. Kudryashov]

What's wrong with longer import lines?

[Scott Morrison]

Fair point. If we're going to have ImportGraph in addition to Cache soon, would everyone prefer that both be moved until Util? I can probably also move the unhelpfully-named MathlibExtras, which manages the additional caching for exact? and rw?.

[Mario Carneiro]

I think the better approach here would be to set the src_dir for the lean_lib Cache to "Util" instead of ".". Then you can still name the module Cache and lake will look in Util/Cache.lean for it

[Mario Carneiro]

(I know that this exists because I recently had cause to reimplement this logic for a lake exe cache rewrite)

[Scott Morrison]

Okay, I've moved everything into the Util directory in #5787.

[Scott Morrison]

That PR also moves the MathlibExtras top-level directory (which handles the special caching infrastructure for apply? and rw?) into Util, and also renames it TacticCaches. This constitutes most of the diff, and I'm a bit worried it will introduce regressions in these special caches. I could also change the PR to just leave that stuff alone for now, hoping for a better solution later (e.g. after the new cache!).