Retrospectively adding `[blueprint]` dependency

[hanwenzhu]

Currently, this works well in a single file:

theorem a
@[blueprint] theorem b := ... a ...
attribute [blueprint] a

in that a is inferred as a dependency of b.

However, if this is split to multiple files, there are particular arrangements where it might not work:

-- A.lean
theorem a
@[blueprint] theorem b := ... a ...

-- B.lean
attribute [blueprint] a

because the blueprint generated from A only considers the content in A, so in the blueprint, b does not depend on a.

This can arise naturally, such as when a is in Mathlib, while b and c are in separate files that do not import each other, but both b and c use a. There is no current good place the attribute [blueprint] a command.

A fix is relatively simple: in Load.lean, change runEnvOfImports #[module] to runEnvOfImports allModules where allModules is passed in from the Lake facet. Then attribute [blueprint] a can be written anywhere (downstream/upstream of/unrelated to b and c) in the entire project.

However, implementing this might break the incremental build logic of module facet :blueprint, in that the :blueprint build result of an earlier module actually depends on a downstream module. This might suggest a large refactor away from single-module-based builds completely, and only exposing a library (not module) facet.