From 2d27691c662b45e5005c9e68006121bf3111dfe0 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 17 Oct 2024 11:28:44 +0200 Subject: [PATCH] update moddoc --- src/Lean/Linter/UnusedVariables.lean | 58 +++++++++++++++++----------- 1 file changed, 36 insertions(+), 22 deletions(-) diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index aeb60ebac7dc..f7b19d16f20f 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -10,41 +10,55 @@ set_option linter.missingDocs true -- keep it documented /-! # Unused variable Linter -This file implements the unused variable linter, which runs automatically on all commands -and reports any local variables that are never referred to, using information from the info tree. - -It is not immediately obvious but this is a surprisingly expensive check without some optimizations. -The main complication is that it can be difficult to determine what constitutes a "use". -For example, we would like this to be considered a use of `x`: +This file implements the unused variable linter, which runs automatically on all +commands and reports any local variables that are never referred to, using +information from the info tree. + +It is not immediately obvious but this is a surprisingly expensive check without +some optimizations. The main complication is that it can be difficult to +determine what constitutes a "use" apart from direct references to a variable +that we can easily find in the info tree. For example, we would like this to be +considered a use of `x`: ``` def foo (x : Nat) : Nat := by assumption ``` -The final proof term is `fun x => x` so clearly `x` was used, but we can't make use of this because -the final proof term is after we have abstracted over the original `fvar` for `x`. If we look -further into the tactic state we can see the `fvar` show up in the instantiation to the original -goal metavariable `?m : Nat := x`, but it is not always the case that we can follow metavariable -instantiations to determine what happened after the fact, because tactics might skip the goal -metavariable and instantiate some other metavariable created prior to it instead. - -Instead, we use a (much more expensive) overapproximation, which is just to look through the entire -metavariable context looking for occurrences of `x`. We use caching to ensure that this is still -linear in the size of the info tree, even though there are many metavariable contexts in all the -intermediate stages of elaboration; these are highly similar and make use of `PersistentHashMap` -so there is a lot of subterm sharing we can take advantage of. +The final proof term is `fun x => x` so clearly `x` was used, but we can't make +use of this because the final proof term is after we have abstracted over the +original `fvar` for `x`. Instead, we make sure to store the proof term before +abstraction but after instantiation of mvars in the info tree and retrieve it in +the linter. Using the instantiated term is very important as redoing that step +in the linter can be prohibitively expensive. The downside of special-casing the +definition body in this way is that while it works for parameters, it does not +work for local variables in the body, so we ignore them by default if any tactic +infos are present (`linter.unusedVariables.analyzeTactics`). + +If we do turn on this option and look further into the tactic state, we can see +the `fvar` show up in the instantiation to the original goal metavariable +`?m : Nat := x`, but it is not always the case that we can follow metavariable +instantiations to determine what happened after the fact, because tactics might +skip the goal metavariable and instantiate some other metavariable created prior +to it instead. Instead, we use a (much more expensive) overapproximation, which +is just to look through the entire metavariable context looking for occurrences +of `x`. We use caching to ensure that this is still linear in the size of the +info tree, even though there are many metavariable contexts in all the +intermediate stages of elaboration; these are highly similar and make use of +`PersistentHashMap` so there is a lot of subterm sharing we can take advantage +of. ## The `@[unused_variables_ignore_fn]` attribute -Some occurrences of variables are deliberately unused, or at least we don't want to lint on unused -variables in these positions. For example: +Some occurrences of variables are deliberately unused, or at least we don't want +to lint on unused variables in these positions. For example: ``` def foo (x : Nat) : (y : Nat) → Nat := fun _ => x -- ^ don't lint this unused variable because it is public API ``` -They are generally a syntactic criterion, so we allow adding custom `IgnoreFunction`s so that -external syntax can also opt in to lint suppression, like so: +They are generally a syntactic criterion, so we allow adding custom +`IgnoreFunction`s so that external syntax can also opt in to lint suppression, +like so: ``` macro (name := foobarKind) "foobar " name:ident : command => `(def foo ($name : Nat) := 0)