Commit 2026-10-20 18:25 f48d5f55

fix(Linter/UnusedTactic): don't use IO.Ref for extensibility (#42536) This PR cleans up the unused tactic linter extensibility implementation. Previously, this was implemented using a PersistentEnvExtension and an IO.Ref. The problem with the IO.Ref is that it creates "spooky action at a distance": a command later in the file can affect what happens earlier in the file. Instead, we can allow both local and global modifications using a SimpleScopedEnvExtension. Previously, the list of exceptions was unnaturally split into the two files. This PR makes it into just a single list. Additionally:

• #allow_unused_tactic is deprecated in favour of allow_unused_tactic
• We put a namespace around the change? syntax, so that change? is not anymore a declared constant.