bench!

PR summary fb131a4c00

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

./scripts/reporting/technical-debt-metrics.sh pr_summary

Thanks, this looks like the right direction for the recursive-hypothesis case.

One bounded edge-case question before merge: this change now preserves every isAuxDecl unconditionally inside getVarsToClear. Is the intended semantics of clear * - now “always retain auxiliary declarations”, analogous to how instances are preserved, or is the goal specifically to protect recursion-critical aux decls?

I’m asking because the current test clearly covers the motivating recursive example, but the implementation change is slightly broader than that example. If the broader semantics are intended, a short note in the docstring/test rationale may be enough.

Thanks, this looks like the right direction for the recursive-hypothesis case.

One bounded edge-case question before merge: this change now preserves every isAuxDecl unconditionally inside getVarsToClear. Is the intended semantics of clear * - now “always retain auxiliary declarations”, analogous to how instances are preserved, or is the goal specifically to protect recursion-critical aux decls?

I’m asking because the current test clearly covers the motivating recursive example, but the implementation change is slightly broader than that example. If the broader semantics are intended, a short note in the docstring/test rationale may be enough.

Good point! The description of the PR is very focussed on the recursion case in order to be specific however the primary motive is to improve the user friendliness of clear * - in that it only clears stuff which hasn't been chosen to be hidden. The expectation is that if something is chosen to be an auxDecl and so hidden then there should be another mechanism to remove this, like nonrec for recursive auxDecl. About all other varied possibilities, I'm sure I don't have the experience to know them all.

I'll improve the docstring. Any suggestions?

One small wording suggestion, if it matches your intent: maybe make the rationale slightly more explicit than the recursive example.

For example, something like:

"Returns the free variable IDs that can be cleared, excluding those in the preserve list, class instances, and hidden auxiliary declarations (for example recursive hypotheses). The intent is that clear * - only clears user-visible local declarations; hidden auxiliary declarations should be handled by more specific mechanisms when needed."

That seemed to match your explanation that the recursion case is the motivating example, but the intended behavior is broader.

If I remember correctly, this PR had some zulip discussion about it. Can you also link that in the PR description, so future readers can find it more easily? Thanks!

If I remember correctly, this PR had some zulip discussion about it. Can you also link that in the PR description, so future readers can find it more easily? Thanks!

Good thinking. Done!

This PR/issue depends on:

• [Merged by Bors] - chore(AlgebraicGeometry): remove use of clear*- from isClosedMap_iff_specializingMap #36961
• [Merged by Bors] - chore: remove superfluous clearExcept call #36966
  By Dependent Issues (🤖). Happy coding!

Yes, this seems reasonable to me. Thanks for making the intended broader semantics explicit in the docstrings and for linking the Zulip discussion as well.