This works fine in Nix because those package names are the names of derivations that themselves pin a given version of said packages.
In practice, the default set is expected to be somewhat internally consistent, so that you can just use the package names to refer to the "most recent consistent set". But if need arises, you can also override individual packages to pin them at a different version than the upstream-provided one.
Indeed trying tactics in general can be unsatisfactory if you 1) don't let users enrich the set of tactics tried 2) don't let users prevent some things from being tried.
For your other issue, I am thinking about ways to hide hypotheses in the editor, without having to clear them in the actual code. This way they are still here if you need them, but they don't eat some of your precious brain space while they are irrelevant (huh) to your current work.
Thanks for your 2 cts! Maybe I'll think about this threshold idea now!
In practice, the default set is expected to be somewhat internally consistent, so that you can just use the package names to refer to the "most recent consistent set". But if need arises, you can also override individual packages to pin them at a different version than the upstream-provided one.