feat: shake: make Mathlib-ready

[Kha]

This PR implements new flags and annotations for shake for use in Mathlib:

Options:
--keep-implied
Preserves existing imports that are implied by other imports and thus not technically needed
anymore

--keep-prefix
If an import X would be replaced in favor of a more specific import X.Y... it implies,
preserves the original import instead. More generally, prefers inserting import X even if it
was not part of the original imports as long as it was in the original transitive import closure
of the current module.

--keep-public
Preserves all public imports to avoid breaking changes for external downstream modules

--add-public
Adds new imports as public if they have been in the original public closure of that module.
In other words, public imports will not be removed from a module unless they are unused even
in the private scope, and those that are removed will be re-added as public in downstream
modules even if only needed in the private scope there. Unlike --keep-public, this may
introduce breaking changes but will still limit the number of inserted imports.

Annotations:
The following annotations can be added to Lean files in order to configure the behavior of
shake. Only the substring shake: directly followed by a directive is checked for, so multiple
directives can be mixed in one line such as -- shake: keep-downstream, shake: keep-all, and they
can be surrounded by arbitrary comments such as -- shake: keep (metaprogram output dependency).

• module -- shake: keep-downstream:
  Preserves this module in all (current) downstream modules, adding new imports of it if needed.

• module -- shake: keep-all:
  Preserves all existing imports in this module as is. New imports now needed because of upstream
  changes may still be added.

• import X -- shake: keep:
  Preserves this specific import in the current module. The most common use case is to preserve a
  public import that will be needed in downstream modules to make sense of the output of a
  metaprogram defined in this module. For example, if a tactic is defined that may synthesize a
  reference to a theorem when run, there is no way for shake to detect this by itself and the
  module of that theorem should be publicly imported and annotated with keep in the tactic's
  module.

  public import X  -- shake: keep (metaprogram output dependency)
  
  ...
  
  elab \"my_tactic\" : tactic => do
    ... mkConst ``f -- `f`, defined in `X`, may appear in the output of this tactic
  

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-03 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-04 14:30:34)

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-11496 has successfully built against this PR. (2025-12-04 15:32:56) View Log