Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
coqbot-app merged 2 commits into from
Mar 19, 2025
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0c7fb9c
search.ml annotate filter functions to make clear why there are unuse…
SkySkimmer Mar 12, 2025
0b112db
Search: don't search local defs (unless Unset Search Blacklist Locals)
SkySkimmer Mar 12, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions doc/changelog/08-vernac-commands-and-options/20349-search-filter-local.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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).
6 changes: 6 additions & 0 deletions doc/sphinx/proof-engine/vernacular-commands.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Copy link
Contributor

@Villetaneuse Villetaneuse Mar 18, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it children instead of parents?

Copy link
Contributor Author

@SkySkimmer SkySkimmer Mar 18, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's parents. ie

Module M.
Local Definition foo := ...
Module N.
Search ...

M.foo is not excluded because M is parent of the current module M.N.

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`,
Expand Down
11 changes: 11 additions & 0 deletions test-suite/output/Search.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
20 changes: 20 additions & 0 deletions test-suite/output/Search.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
2 changes: 2 additions & 0 deletions vernac/declare.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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} *)

Expand Down
37 changes: 23 additions & 14 deletions vernac/search.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -172,25 +175,31 @@ let prioritize_search seq fn =

(** This function tries to see whether the conclusion matches a pattern.
FIXME: this is quite dummy, we may find a more efficient algorithm. *)
let rec pattern_filter pat ref env sigma typ =
let rec pattern_filter pat env sigma typ =
let typ = Termops.strip_outer_cast sigma typ in
if Constr_matching.is_matching env sigma pat typ then true
else match EConstr.kind sigma typ with
| Prod (_, _, typ)
| LetIn (_, _, _, typ) -> pattern_filter pat ref env sigma typ
| LetIn (_, _, _, typ) -> pattern_filter pat env sigma typ
| _ -> false

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

(** Whether a reference is blacklisted *)
let blacklist_filter 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 ())
let is_local_ref : GlobRef.t -> bool = function
| ConstRef c -> Declare.is_local_constant c
| IndRef _ | ConstructRef _ | VarRef _ -> false

let module_filter mods ref kind env sigma typ =
(** Whether a reference is blacklisted *)
let blacklist_filter : filter_function = fun ref kind env sigma typ ->
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
let sl = dirpath sp in
match mods with
Expand All @@ -203,7 +212,7 @@ let module_filter mods ref kind env sigma typ =

let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref)

let search_filter query gr kind env sigma typ = match query with
let search_filter : _ -> filter_function = fun query gr kind env sigma typ -> match query with
| GlobSearchSubPattern (where,head,pat) ->
let open Context.Rel.Declaration in
let rec collect env hyps typ =
Expand All @@ -230,7 +239,7 @@ let search_filter query gr kind env sigma typ = match query with
let search_pattern env sigma pat mods pr_search =
let filter ref kind env sigma typ =
module_filter mods ref kind env sigma typ &&
pattern_filter pat ref env sigma (EConstr.of_constr typ) &&
pattern_filter pat env sigma (EConstr.of_constr typ) &&
blacklist_filter ref kind env sigma typ
in
let iter ref kind env sigma typ =
Expand All @@ -253,8 +262,8 @@ let search_rewrite env sigma pat mods pr_search =
let pat2 = rewrite_pat2 pat in
let filter ref kind env sigma typ =
module_filter mods ref kind env sigma typ &&
(pattern_filter pat1 ref env sigma (EConstr.of_constr typ) ||
pattern_filter pat2 ref env sigma (EConstr.of_constr typ)) &&
(pattern_filter pat1 env sigma (EConstr.of_constr typ) ||
pattern_filter pat2 env sigma (EConstr.of_constr typ)) &&
blacklist_filter ref kind env sigma typ
in
let iter ref kind env sigma typ =
Expand Down Expand Up @@ -310,7 +319,7 @@ let interface_search env sigma =
let (name, tpe, subtpe, mods, blacklist) =
extract_flags [] [] [] [] false flags
in
let filter_function ref env sigma constr =
let filter_function ref kind env sigma constr =
let id = Names.Id.to_string (Nametab.basename_of_global ref) in
let path = Libnames.dirpath (Nametab.path_of_global ref) in
let toggle x b = if x then b else not b in
Expand Down Expand Up @@ -359,7 +368,7 @@ let interface_search env sigma =
ans := answer :: !ans;
in
let iter ref kind env sigma typ =
if filter_function ref env sigma typ then print_function ref env sigma typ
if filter_function ref kind env sigma typ then print_function ref env sigma typ
in
let () = generic_search env sigma iter in
!ans
Loading