diff --git a/doc/changelog/08-vernac-commands-and-options/19808-create-hintdb.rst b/doc/changelog/08-vernac-commands-and-options/19808-create-hintdb.rst new file mode 100644 index 000000000000..042d9ac178f2 --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/19808-create-hintdb.rst @@ -0,0 +1,4 @@ +- **Changed:** + :cmd:`Create HintDb` does not erase pre-existing hint databases + (`#19808 `_, + by Gaƫtan Gilbert). diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index 8a47a5bf82a6..f1c96da78b99 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -329,7 +329,9 @@ and `Constants`, while implicitly created databases have the `Opaque` setting. .. cmd:: Create HintDb @ident {? discriminated } - Creates a new hint database named :n:`@ident`. The database is + If a hint database named :n:`@name` already exists, do nothing. + + Otherwise creates a new hint database named :n:`@ident`. The database is implemented by a Discrimination Tree (DT) that serves as a filter to select the lemmas that will be applied. When discriminated, the DT uses transparency information to decide if a constant should considered rigid for @@ -340,6 +342,13 @@ and `Constants`, while implicitly created databases have the `Opaque` setting. By default, hint databases are undiscriminated. + .. warn:: @ident already exists and is {? not } discriminated + :name: mismatched-hint-db + + `Create HintDb` will not change whether a pre-existing database + is discriminated. + + Hint databases defined in the Rocq standard library ``````````````````````````````````````````````````` diff --git a/tactics/hints.ml b/tactics/hints.ml index 54cbb0538dd7..9ec4b4f6bd3e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1101,8 +1101,17 @@ type db_obj = { db_ts : TransparentState.t; } -let cache_db {db_name=name; db_use_dn=b; db_ts=ts} = - searchtable_add (name, Hint_db.empty ~name ts b) +let warn_mismatch_create_hintdb = CWarnings.create ~name:"mismatched-hint-db" ~category:CWarnings.CoreCategories.automation + Pp.(fun {db_name;db_use_dn} -> + str "Hint Db " ++ str db_name ++ str " already exists and " ++ + (if db_use_dn then str "is not" else str "is") ++ str " discriminated.") + +let cache_db ({db_name=name; db_use_dn=b; db_ts=ts} as o) = + match searchtable_map name with + | exception Not_found -> searchtable_add (name, Hint_db.empty ~name ts b) + | db -> + (* AFAICT all DBs start with full transparent state so nothing to do with it *) + if Hint_db.use_dn db <> b then warn_mismatch_create_hintdb o let load_db _ x = cache_db x