Create HintDb does not erase pre-existing hint db

doc/changelog/08-vernac-commands-and-options/19808-create-hintdb.rst

@@ -0,0 +1,4 @@
+- **Changed:**
+  :cmd:`Create HintDb` no longer erases pre-existing hint databases
+  (`#19808 <https://github.com/coq/coq/pull/19808>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proofs/automatic-tactics/auto.rst

@@ -320,7 +320,8 @@ 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 there is no hint database named :n:`@name`, creates a new hint database
+   with that name.  Otherwise, does nothing.  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
@@ -331,6 +332,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
 ```````````````````````````````````````````````````
 

tactics/hints.ml

@@ -1101,8 +1101,20 @@ 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 ->
+    (* Explicit DBs start with full TS, implicit DBs start with empty TS
+       This should probably be controllable in Create Hint Db,
+       otherwise we have to do eg "Create HintDb foo. Hint Constants Opaque : foo."
+       and if someone else creates foo and puts some transparency hints they will be overwritten. *)
+    if Hint_db.use_dn db <> b then warn_mismatch_create_hintdb o
 
 let load_db _ x = cache_db x
 

test-suite/success/Hints.v

@@ -202,3 +202,29 @@ Section HintTransparent.
   Qed.
 
 End HintTransparent.
+
+Module RepeatCreat.
+  Axiom T : Type.
+  Axiom v : T.
+
+  Set Warnings "+mismatched-hint-db".
+
+  (* if this fails it means the db already exists as a discriminated db *)
+  Succeed Create HintDb repeated.
+
+  Create HintDb repeated discriminated.
+
+  Fail Definition foo : T := ltac:(eauto with foo).
+
+  Hint Resolve v : foo.
+  Definition foo : T := ltac:(eauto with foo).
+
+  Create HintDb repeated discriminated.
+  (* hint is still there *)
+  Definition foo' : T := ltac:(eauto with foo).
+
+  Fail Create HintDb repeated.
+
+  (* implicit hint db *)
+  Fail Create HintDb foo discriminated.
+End RepeatCreat.