From 1a5e5534ad9321f0b88e27f6e6bfab51709aa534 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 30 May 2024 15:21:59 +0200 Subject: [PATCH] [coq] [fix] Install .glob files This seems like an omission from the beginning, I'm surprised this wasn't a problem for anyone until now. Signed-off-by: Emilio Jesus Gallego Arias --- doc/changes/10602.md | 1 + src/dune_rules/coq/coq_module.ml | 19 ++++++++++++------- 2 files changed, 13 insertions(+), 7 deletions(-) create mode 100644 doc/changes/10602.md diff --git a/doc/changes/10602.md b/doc/changes/10602.md new file mode 100644 index 000000000000..4dd61882fd7c --- /dev/null +++ b/doc/changes/10602.md @@ -0,0 +1 @@ +- install `.glob` files for Coq theories too (#10602, @ejgallego) diff --git a/src/dune_rules/coq/coq_module.ml b/src/dune_rules/coq/coq_module.ml index d302d4667732..2ef2d8abff83 100644 --- a/src/dune_rules/coq/coq_module.ml +++ b/src/dune_rules/coq/coq_module.ml @@ -76,6 +76,17 @@ let glob_file x ~obj_dir = Path.Build.relative vo_dir (x.name ^ ".glob") ;; +(* As of today we do the same for build and install, it used not to be + the case *) +let standard_obj_files ~(mode : Coq_mode.t) _obj_files_mode name = + let ext, glob = + match mode with + | VosOnly -> ".vos", [] + | _ -> ".vo", [ name ^ ".glob" ] + in + [ name ^ ext ] @ glob +;; + (* XXX: Remove the install .coq-native hack once rules can output targets in multiple subdirs *) let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode = @@ -92,13 +103,7 @@ let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode = cmxs_obj | VoOnly | VosOnly | Legacy -> [] in - let obj_files = - match obj_files_mode with - | Build when mode = VosOnly -> [ x.name ^ ".vos" ] - | Build -> [ x.name ^ ".vo"; x.name ^ ".glob" ] - | Install when mode = VosOnly -> [ x.name ^ ".vos" ] - | Install -> [ x.name ^ ".vo" ] - in + let obj_files = standard_obj_files ~mode obj_files_mode x.name in List.map obj_files ~f:(fun fname -> Path.Build.relative vo_dir fname, Filename.concat install_vo_dir fname) @ native_objs