[mltop] Store digest of modules used to compile files.

This should allow digest-based builds to work correctly.

Fixes #10874

For now, we store the digest of the module selected, this means that
vo files loading modules will have different digests depending on
whether the `native` or `byte` version was used.

If that is a problem we can improve this tho; for example we could
disable the digest in those cases.

The code could be better, and indeed `Mltop` could enjoy a nice
cleanup, I will likely do some when I add support for `Fl_dynload`.

1 files changed, 21 insertions, 6 deletions

diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 9c18441d9c..bd361a76c1 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -11,7 +11,6 @@
 open CErrors
 open Util
 open Pp
-open Libobject
 open System
 
 (* Code to hook Coq into the ML toplevel -- depends on having the
@@ -334,23 +333,38 @@ let _ =
 
 (* Liboject entries of declared ML Modules *)
 
+(* Digest of module used to compile the file *)
+type ml_module_digest =
+  | NoDigest
+  | AnyDigest of Digest.t             (* digest of any used cma / cmxa *)
+
 type ml_module_object = {
   mlocal : Vernacexpr.locality_flag;
-  mnames : string list
+  mnames : (string * ml_module_digest) list
 }
 
+let add_module_digest m =
+  try
+    let file = file_of_name m in
+    let path, file = System.where_in_path ~warn:false !coq_mlpath_copy file in
+    m, AnyDigest (Digest.file file)
+  with
+  | Not_found ->
+    m, NoDigest
+
 let cache_ml_objects (_,{mnames=mnames}) =
-  let iter obj = trigger_ml_object true true true obj in
+  let iter (obj, _) = trigger_ml_object true true true obj in
   List.iter iter mnames
 
 let load_ml_objects _ (_,{mnames=mnames}) =
-  let iter obj = trigger_ml_object true false true obj in
+  let iter (obj, _) = trigger_ml_object true false true obj in
   List.iter iter mnames
 
 let classify_ml_objects ({mlocal=mlocal} as o) =
-  if mlocal then Dispose else Substitute o
+  if mlocal then Libobject.Dispose else Libobject.Substitute o
 
-let inMLModule : ml_module_object -> obj =
+let inMLModule : ml_module_object -> Libobject.obj =
+  let open Libobject in
   declare_object
     {(default_object "ML-MODULE") with
       cache_function = cache_ml_objects;
@@ -360,6 +374,7 @@ let inMLModule : ml_module_object -> obj =
 
 let declare_ml_modules local l =
   let l = List.map mod_of_name l in
+  let l = List.map add_module_digest l in
   Lib.add_anonymous_leaf ~cache_first:false (inMLModule {mlocal=local; mnames=l})
 
 let print_ml_path () =