chore: run lake shake --fix

[thorimur]

This PR runs lake shake --fix, except for ImportGraph.lean and ImportGraph.Tools, which are left unchanged.

It also updates tests which depend on the import structure of this repo (which is now different).

---

• depends on: fix: do not import Lake internals downstream #159

[joneugster]

Thanks! Let me take this as an inspiration to look at the imports more carfully. Meant to do that anyways once your PRs were merged.

[joneugster]

I thought last time I looked at this it was necessary to public import Cli or the command wouldnt run. Forgot what the issue was though

[thorimur]

lake exe graph seems to work for me, I'm not sure! Feel free to revert, though!

[JovanGerb]

I used assert_not_imported to figure out what stuff mathlib imports transitively through ImportGraph, and I see the following chain of imports that all come just from ImportGraphs. It would be great if we could get rid of these excessive imports in mathlib, as mathlib doesn't depend on most of these things, and they are slowing down imports:

the module 'Std.Data.HashSet.Lemmas' is (transitively) imported via
Std.Data.HashSet.Lemmas,
  which is imported by Std.Data.Iterators.Lemmas.Consumers.Set,
  which is imported by Std.Data.Iterators.Lemmas.Consumers,
  which is imported by Std.Data.Iterators.Lemmas.Combinators.TakeWhile,
  which is imported by Std.Data.Iterators.Lemmas.Combinators,
  which is imported by Std.Data.Iterators.Lemmas,
  which is imported by Std.Data.Iterators,
  which is imported by Std.Data.DHashMap.IteratorLemmas,
  which is imported by Std.Data.DHashMap,
  which is imported by Std.Data,
  which is imported by Std.Sync.CancellationToken,
  which is imported by Std.Sync.CancellationContext,
  which is imported by Std.Async.ContextAsync,
  which is imported by Std.Async,
  which is imported by Std.Http.Data.Body.Basic,
  which is imported by Std.Http.Data.Body.Replayable,
  which is imported by Std.Http.Data.Body.Any,
  which is imported by Std.Http.Data.Body.Stream,
  which is imported by Std.Http.Data.Body,
  which is imported by Std.Http.Data,
  which is imported by Std.Http.Protocol.H1.Config,
  which is imported by Std.Http.Protocol.H1.Parser,
  which is imported by Std.Http.Protocol.H1.Error,
  which is imported by Std.Http.Protocol.H1.Reader,
  which is imported by Std.Http.Protocol.H1,
  which is imported by Std.Http.Server.Config,
  which is imported by Std.Http.Server.Connection,
  which is imported by Std.Http.Server,
  which is imported by Std.Http.Test.Helpers,
  which is imported by Std.Http,
  which is imported by Lean.Util.ProfilerServer,
  which is imported by Lean.Elab.Frontend,
  which is imported by Lake.Load.Lean.Elab,
  which is imported by Lake.Load.Lean,
  which is imported by Lake.Load.Package,
  which is imported by Lake.Load.Resolve,
  which is imported by Lake.Load.Workspace,
  which is imported by ImportGraph.Lake,
  which is imported by ImportGraph.WorkspaceModel.Base,
  which is imported by ImportGraph.WorkspaceModel.Model,
  which is imported by ImportGraph.WorkspaceModel.Build,
  which is imported by ImportGraph.Shake.Workspace,
  which is imported by ImportGraph.Tools.FindHome,
  which is imported by ImportGraph.Tools,
  which is imported by Mathlib.Init,

[thorimur]

Hmm, this is a bit difficult because these are (mostly) all just modules for which we load (only) the IR due to meta import ignoring module system annotations. I.e., we don't load the olean/put these constants in the (kernel) environment.

-- in Mathlib.Init

open Lean Elab Command

/-- info: false -/ -- `*.olean` not loaded
#guard_msgs in
run_cmd
  let some idx := (← getEnv).getModuleIdx? `Std.Data.HashSet.Lemmas | throwError "not found"
  logInfo m!"{(← getEnv).header.modules[idx]!.hasData}"

So I'm not sure how to lift the necessary constants to the meta level without also loading their IR 🤔

Though, it's probably also worth benching just to confirm that these imports really are what's slowing down mathlib. (That might involve temporarily "breaking" the elaborator code by allowing a relaxed meta check, so that we still produce the code but allow ourselves to break the import chain, then benching.)

[JovanGerb]

Re: benchmarking, can't we just remove the import of ImportGraph from Mathlib and then benchmark? Or is there anything else that ImportGraph does that could slow down mathlib?

[JovanGerb]

What does meta import ignore? I think it is intended behaviour that a meta import automatically also meta imports all private transitive imports, because in theory the IR of those modules could be required.

[JovanGerb]

I think it is clear that ImportGraph doesn't need lemmas about iterators. The question is just at what point in the import chain we have a redundant import. Can it be fixed here, or should we make a PR to modify Lake?

[thorimur]

It's maybe a merely technical point if this is slowing things down one way or another, but it might be worth clarifying on this PR that meta import doesn't strictly meta import private transitive imports, it only loads their IR.

So indeed ImportGraph does not have lemmas about iterators, it only has the IR from that module loaded.

I do think maybe Sebastian is thinking about this sort of thing based on conversations around meta, since it does kind of defeat the point of the module system if we have to micromanage upstream private imports in order to get good performance...

[thorimur]

Re: benchmarking, can't we just remove the import of ImportGraph from Mathlib and then benchmark? Or is there anything else that ImportGraph does that could slow down mathlib?

Well ImportGraph loads its own modules/IR, so if it's loading all the code in ImportGraph proper that's the issue, or some other issue we're not thinking of, we'd miss that. Though I'm not sure how likely this is.

[JovanGerb]

Let's benchmark mathlib without ImportGraph after this PR is merged, to see the effect of the import. I suspect that even if we only load their IR, there is still a cost to depending on more files. (See also leanprover-community/mathlib4#40222 and leanprover-community/mathlib4#40625 which collectively sped up mathlib by over 5% by reducing imports)