Search: don't search local defs (unless Unset Search Blacklist Locals)

Author: SkySkimmer

doc/changelog/08-vernac-commands-and-options/20349-search-filter-local.rst

@@ -0,0 +1,5 @@
+- **Changed:**
+  :cmd:`Search` ignores lemmas declared with :attr:`local` unless
+  new flag :flag:`Search Blacklist Locals` is unset
+  (`#20349 <https://github.com/coq/coq/pull/20349>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -369,6 +369,12 @@ described elsewhere
 
          SearchRewrite (_ + _ + _).
 
+.. flag:: Search Blacklist Locals
+
+   By default :cmd:`Search` excludes lemmas declared with :attr:`local` from its results
+   (except for those from the current module or its parents).
+   Unsetting this :term:`flag` will include such lemmas in the results.
+
 .. table:: Search Blacklist @string
 
    This :term:`table` specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`,

test-suite/output/Search.out

@@ -451,3 +451,14 @@ plus_O_n: forall n : nat, 0 + n = n
 plus_n_Sm: forall n m : nat, S (n + m) = n + S m
 plus_Sn_m: forall n m : nat, S n + m = S (n + m)
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
+should say both t and t_alias
+- : Init.unit = ()
+t: T
+t_alias: T
+should say only t
+- : Init.unit = ()
+BlacklistLocals.t: BlacklistLocals.T
+should say both t and t_alias
+- : Init.unit = ()
+BlacklistLocals.t_alias: BlacklistLocals.T
+BlacklistLocals.t: BlacklistLocals.T

test-suite/output/Search.v

@@ -52,3 +52,23 @@ Search "+".
 Search hyp:bool -headhyp:bool.
 Search concl:bool -headconcl:bool.
 Search [ is:Definition headconcl:nat | is:Lemma (_ + _) ].
+
+(* used to print something between search outputs, otherwise we can't
+   tell which lines are from which command *)
+Require Import Ltac2.Printf.
+
+Module BlacklistLocals.
+  Axiom T : Type.
+  Axiom t : T.
+  Local Definition t_alias := t.
+
+  Ltac2 Eval printf "should say both t and t_alias".
+  Search T.
+End BlacklistLocals.
+
+Ltac2 Eval printf "should say only t".
+Search BlacklistLocals.T.
+
+Unset Search Blacklist Locals.
+Ltac2 Eval printf "should say both t and t_alias".
+Search BlacklistLocals.T.

vernac/declare.mli

@@ -625,6 +625,8 @@ val program_inference_hook : Environ.env -> Evd.evar_map -> Evar.t -> (Evd.evar_
 end
 
 val is_local_constant : Constant.t -> bool
+(** [true] on constants declared Local and not from the current
+    interactive module (or its parents). *)
 
 (** {6 For internal support, do not use}  *)
 

vernac/search.ml

@@ -51,6 +51,9 @@ module SearchBlacklist =
         str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s
      end)
 
+let { Goptions.get = blacklist_locals } =
+  Goptions.declare_bool_option_and_ref ~key:["Search";"Blacklist";"Locals"] ~value:true ()
+
 (* The functions iter_constructors and iter_declarations implement the behavior
    needed for the Rocq searching commands.
    These functions take as first argument the procedure
@@ -184,11 +187,17 @@ let full_name_of_reference ref =
   let (dir,id) = repr_path (Nametab.path_of_global ref) in
   DirPath.to_string dir ^ "." ^ Id.to_string id
 
+let is_local_ref : GlobRef.t -> bool = function
+  | ConstRef c -> Declare.is_local_constant c
+  | IndRef _ | ConstructRef _ | VarRef _ -> false
+
 (** Whether a reference is blacklisted *)
 let blacklist_filter : filter_function = fun ref kind env sigma typ ->
-  let name = full_name_of_reference ref in
-  let is_not_bl str = not (String.string_contains ~where:name ~what:str) in
-  CString.Set.for_all is_not_bl (SearchBlacklist.v ())
+  if blacklist_locals() && is_local_ref ref then false
+  else
+    let name = full_name_of_reference ref in
+    let is_not_bl str = not (String.string_contains ~where:name ~what:str) in
+    CString.Set.for_all is_not_bl (SearchBlacklist.v ())
 
 let module_filter : _ -> filter_function = fun mods ref kind env sigma typ ->
   let sp = Nametab.path_of_global ref in