[coq] Fix coqlib file scanning. (#7954)

The old code did indeed was nonsense, and among others was filtering
all the files due to the `String.contains d '.'` condition.

I wonder how the test for updating a file in user-contrib did pass
tho, that seems pretty strange, as indeed we were not adding any .vo
file to the .vo file list on the user-contrib deps, so this deserves
more investigation.

Fixes #7893 , thanks to Karl Palmskog for testing and detailed report.

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
Co-authored-by: Emilio Jesus Gallego Arias <[email protected]>

CHANGES.md

@@ -6,6 +6,9 @@
 
 - Respect `-p` / `--only-packages` for `melange.emit` artifacts (#7849, @anmonteiro)
 
+- Fix scanning of Coq installed files (@ejgallego, reported by
+  @palmskog, #7895 , fixes #7893)
+
 3.8.1 (2023-06-05)
 ------------------
 

src/dune_rules/coq/coq_lib.ml

@@ -152,7 +152,7 @@ and Legacy : sig
     ; implicit : bool (* Only useful for the stdlib *)
     ; installed_root : Path.t (* ; libraries : (Loc.t * Lib.t) list Resolve.t *)
     ; vo : Path.t list
-    ; cmxs : Path.t list
+    ; cmxs_directories : Path.t list
     }
 
   val to_dyn : t -> Dyn.t
@@ -171,27 +171,24 @@ end = struct
     ; implicit : bool (* Only useful for the stdlib *)
     ; installed_root : Path.t (* ; libraries : (Loc.t * Lib.t) list Resolve.t *)
     ; vo : Path.t list
-    ; cmxs : Path.t list
+    ; cmxs_directories : Path.t list
     }
 
-  let to_dyn { boot_id; id; implicit; installed_root; vo; cmxs } =
+  let to_dyn { boot_id; id; implicit; installed_root; vo; cmxs_directories } =
     Dyn.record
       [ ("boot_id", Dyn.option Id.to_dyn boot_id)
       ; ("id", Id.to_dyn id)
       ; ("implicit", Dyn.bool implicit)
       ; ("installed_root", Path.to_dyn installed_root)
       ; ("vo", Dyn.list Path.to_dyn vo)
-      ; ("cmxs", Dyn.list Path.to_dyn cmxs)
-        (* ; ( "libraries" *)
-        (*   , Resolve.to_dyn (Dyn.list (Dyn.pair Loc.to_dyn Lib.to_dyn)) libraries *)
-        (* ) *)
+      ; ("cmxs_directories", Dyn.list Path.to_dyn cmxs_directories)
       ]
 
   let implicit t = t.implicit
 
   let installed_root t = t.installed_root
 
-  let cmxs_directories t = t.cmxs
+  let cmxs_directories t = t.cmxs_directories
 
   let vo t = t.vo
 end
@@ -504,16 +501,17 @@ module DB = struct
     let create_from_stanza coq_db db dir stanza =
       Memo.exec memo (coq_db, db, dir, stanza)
 
-    (* XXX: Memoize? This is pretty cheap so not sure worth the cost *)
+    (* XXX: Memoize? This is pretty cheap so not sure worth the cost,
+       still called too much I have observed, suspicious! *)
     let create_from_coqpath ~boot_id cp =
       let name = Coq_path.name cp in
       let installed_root = Coq_path.path cp in
       let implicit = Coq_path.stdlib cp in
-      let cmxs = Coq_path.cmxs cp in
+      let cmxs_directories = Coq_path.cmxs_directories cp in
       let vo = Coq_path.vo cp in
       let id = Id.create ~path:installed_root ~name:(Loc.none, name) in
       Resolve.Memo.return
-        { Legacy.boot_id; id; implicit; installed_root; vo; cmxs }
+        { Legacy.boot_id; id; implicit; installed_root; vo; cmxs_directories }
 
     module Resolve_result_no_redirect = struct
       (** In our second iteration, we remove all the redirects *)

src/dune_rules/coq/coq_lib.mli

@@ -17,6 +17,22 @@ end
 module Legacy : sig
   type t
 
+  (** For each legacy library, we need two pieces of data:
+
+      - the list of [.vo] files, this is because we need to make the call to
+        [coqdep] depend on it. If due to external action the list of these files
+        changes, coqdep must be re-run. Note that coqdep sometimes checks for
+        [.vo] files and sometimes for [.v] files, which is messy (in principle
+        only checks for [.v] files when compiling the stdlib using make, but
+        YMMV with coqdep code).
+
+      In the case of a [Dune.t] lib, this list is obtained from the [src_root],
+      via [Dir_contents.coq], maybe we should move that function here and make
+      it common.
+
+      - the list of directories containing [.cmxs] files, so we can add them to
+        the loadpath as Coq does for all [user-contrib] *)
+
   (** List of vo files *)
   val vo : t -> Path.t list
 

src/dune_rules/coq/coq_path.ml

@@ -12,6 +12,7 @@ type t =
   ; path : Path.t
   ; vo : Path.t list
   ; cmxs : Path.t list
+  ; cmxs_directories : Path.t list
   ; stdlib : bool
   }
 
@@ -23,6 +24,8 @@ let vo t = t.vo
 
 let cmxs t = t.cmxs
 
+let cmxs_directories t = t.cmxs_directories
+
 let stdlib t = t.stdlib
 
 let config_path_exn coq_config key =
@@ -48,98 +51,136 @@ let config_path ~default coq_config key =
     (* This should never happen *)
     Code_error.raise "key is not a path" [ (key, Coq_config.Value.to_dyn path) ]
 
-let stdlib_plugins_dir path =
-  let open Memo.O in
-  let path = Path.relative path "plugins" in
-  let* dir_contents =
-    Fs_memo.dir_contents (Path.as_outside_build_dir_exn path)
-  in
-  match dir_contents with
-  | Error _ -> Memo.return []
-  | Ok dir_contents ->
-    let f (d, kind) =
-      match kind with
-      | File_kind.S_DIR | S_LNK -> Some (Path.relative path d)
-      | _ -> None
-    in
-    Memo.return
-      (List.filter_map ~f (Fs_cache.Dir_contents.to_list dir_contents))
-
-let build_user_contrib ~cmxs ~vo ~subpath ~name =
-  let path = subpath in
-  { name; path; cmxs; vo; stdlib = false }
+let build_user_contrib ~cmxs ~cmxs_directories ~vo ~path ~name =
+  { name; path; cmxs; cmxs_directories; vo; stdlib = false }
 
 (* Scanning todos: blacklist? *)
-let scan_vo_cmxs ~path dir_contents =
+let scan_vo_cmxs ~dir dir_contents =
   let f (d, kind) =
     match kind with
-    (* Skip some directories as Coq does, for now '-' and '.' *)
+    (* Skip some files as Coq does, for now files with '-' *)
     | _ when String.contains d '-' -> List.Skip
-    | _ when String.contains d '.' -> Skip
     | (File_kind.S_REG | S_LNK) when Filename.check_suffix d ".cmxs" ->
-      Left (Path.relative path d)
+      Left (Path.relative dir d)
     | (File_kind.S_REG | S_LNK) when Filename.check_suffix d ".vo" ->
-      Right (Path.relative path d)
+      Right (Path.relative dir d)
     | _ -> Skip
   in
   List.filter_partition_map ~f dir_contents
 
 (* Note this will only work for absolute paths *)
 let retrieve_vo_cmxs cps =
-  (List.concat_map ~f:cmxs cps, List.concat_map ~f:vo cps)
+  ( List.concat_map ~f:cmxs cps
+  , List.concat_map ~f:cmxs_directories cps
+  , List.concat_map ~f:vo cps )
+
+module Scan_action = struct
+  type ('prefix, 'res) t =
+       dir:Path.t
+    -> prefix:'prefix
+    -> subresults:'res list
+    -> (Filename.t * File_kind.t) list
+    -> 'res list Memo.t
+end
+
+(** [scan_path ~f ~acc ~prefix ~dir dir_contents] Given
+    [f ~dir
+    ~prefix ~subresults dir_contents], [scan_path] will call [f]
+    forall the subdirs of [dir] with [dir] set to the subpath, [prefix] set to
+    [acc prefix d] for each subdirectory [d] and [subresults] the results of the
+    scanning of children directories *)
+let rec scan_path ~(f : ('prefix, 'res) Scan_action.t) ~acc ~prefix ~dir
+    dir_contents : 'a list Memo.t =
+  let open Memo.O in
+  let f (d, kind) =
+    match kind with
+    (* We skip directories starting by . , this is mainly to avoid
+       .coq-native *)
+    | (File_kind.S_DIR | S_LNK) when d.[0] = '.' -> Memo.return []
+    (* Need to check the link resolves to a directory! *)
+    | File_kind.S_DIR | S_LNK -> (
+      let dir = Path.relative dir d in
+      let* dir_contents =
+        Fs_memo.dir_contents (Path.as_outside_build_dir_exn dir)
+      in
+      match dir_contents with
+      | Error _ -> Memo.return []
+      | Ok dir_contents ->
+        let dir_contents = Fs_cache.Dir_contents.to_list dir_contents in
+        let prefix = acc prefix d in
+        let* subresults = scan_path ~f ~acc ~prefix ~dir dir_contents in
+        f ~dir ~prefix ~subresults dir_contents)
+    | _ -> Memo.return []
+  in
+  Memo.List.concat_map ~f dir_contents
 
-(** [scan_user_path ~prefix path] Note that we already have very similar
-    functionality in [Dir_status] *)
-let rec scan_path ~f ~acc ~prefix path : 'a list Memo.t =
+let scan_path ~f ~acc ~prefix dir =
   let open Memo.O in
   let* dir_contents =
-    Fs_memo.dir_contents (Path.as_outside_build_dir_exn path)
+    Fs_memo.dir_contents (Path.as_outside_build_dir_exn dir)
   in
   match dir_contents with
   | Error _ -> Memo.return []
   | Ok dir_contents ->
     let dir_contents = Fs_cache.Dir_contents.to_list dir_contents in
-    let f (d, kind) =
-      match kind with
-      | File_kind.S_DIR | S_LNK ->
-        let subpath = Path.relative path d in
-        let prefix = acc prefix d in
-        let* subpaths = scan_path ~f ~acc ~prefix subpath in
-        f ~path ~prefix ~subpath ~subpaths dir_contents
-      | _ -> Memo.return []
+    scan_path ~f ~acc ~prefix ~dir dir_contents
+
+(** Scan the plugins in stdlib, returns list of cmxs + list of directories with
+    cmxs *)
+let scan_stdlib_plugins coqcorelib : (Path.t list * Path.t) list Memo.t =
+  let f ~dir ~prefix:() ~subresults dir_contents =
+    let cmxs, _ = scan_vo_cmxs ~dir dir_contents in
+    let res =
+      match cmxs with
+      | [] -> subresults
+      | _ :: _ -> (cmxs, dir) :: subresults
     in
-    Memo.List.concat_map ~f dir_contents
-
-let scan_user_path path =
-  let f ~path ~prefix ~subpath ~subpaths dir_contents =
-    let cmxs, vo = scan_vo_cmxs ~path dir_contents in
-    let cmxs_r, vo_r = retrieve_vo_cmxs subpaths in
-    let cmxs, vo = (cmxs @ cmxs_r, vo @ vo_r) in
-    Memo.return (build_user_contrib ~cmxs ~vo ~subpath ~name:prefix :: subpaths)
+    Memo.return res
+  in
+  let pluginsdir = Path.relative coqcorelib "plugins" in
+  let acc _ _ = () in
+  scan_path ~f ~acc ~prefix:() pluginsdir
+
+(** [scan_user_path path] Note that we already have very similar functionality
+    in [Dir_status] *)
+let scan_user_path root_path =
+  let f ~dir ~prefix ~subresults dir_contents =
+    let cmxs, vo = scan_vo_cmxs ~dir dir_contents in
+    let cmxs_directories = if not (List.is_empty cmxs) then [ dir ] else [] in
+    let cmxs_r, cdir_r, vo_r = retrieve_vo_cmxs subresults in
+    let cmxs, cmxs_directories, vo =
+      (cmxs @ cmxs_r, cmxs_directories @ cdir_r, vo @ vo_r)
+    in
+    Memo.return
+      (build_user_contrib ~cmxs ~cmxs_directories ~vo ~path:dir ~name:prefix
+      :: subresults)
   in
-  scan_path path ~f ~acc:Coq_lib_name.append ~prefix:Coq_lib_name.empty
+  scan_path ~f ~acc:Coq_lib_name.append ~prefix:Coq_lib_name.empty root_path
 
-let scan_vo path =
-  let f ~path ~prefix:_ ~subpath:_ ~subpaths dir_contents =
-    let _, vo = scan_vo_cmxs ~path dir_contents in
-    Memo.return (vo @ subpaths)
+let scan_vo root_path =
+  let f ~dir ~prefix:() ~subresults dir_contents =
+    let _, vo = scan_vo_cmxs ~dir dir_contents in
+    Memo.return (vo @ subresults)
   in
   let acc _ _ = () in
-  scan_path path ~f ~acc ~prefix:()
+  scan_path ~f ~acc ~prefix:() root_path
 
 let of_coq_install coqc =
   let open Memo.O in
   let* coq_config = Coq_config.make ~coqc:(Ok coqc) in
   (* Now we query for coqlib *)
   let coqlib_path = config_path_exn coq_config "coqlib" in
   let coqcorelib = config_path coq_config "coqcorelib" ~default:coqlib_path in
-  let* cmxs = stdlib_plugins_dir coqcorelib in
+  let* stdlib_plugs = scan_stdlib_plugins coqcorelib in
   let* vo = scan_vo coqlib_path in
+  let cmxs, cmxs_directories = List.split stdlib_plugs in
+  let cmxs = List.concat cmxs in
   let stdlib =
     { name = Coq_lib_name.stdlib
     ; path = Path.relative coqlib_path "theories"
     ; vo
     ; cmxs
+    ; cmxs_directories
     ; stdlib = true
     }
   in

src/dune_rules/coq/coq_path.mli

@@ -18,13 +18,21 @@ val name : t -> Coq_lib_name.t
 
 val path : t -> Path.t
 
+(** List of .vo files in a path *)
 val vo : t -> Path.t list
 
+(** Unused for now, maybe be useful for coqdep -modules *)
 val cmxs : t -> Path.t list
 
+(** List of directories that contain .cmxs files and thus need to be passed to
+    Coq using -I *)
+val cmxs_directories : t -> Path.t list
+
+(** Does the path correspond to Coq's stdlib? *)
 val stdlib : t -> bool
 
+(** Build list of Coq paths from a Coq install ([COQLIB] and [coqc -config]) *)
 val of_coq_install : Context.t -> t list Memo.t
 
-(**  *)
+(** Build list of Coq paths from [COQPATH] variable *)
 val of_env : Env.t -> t list Memo.t

test/blackbox-tests/test-cases/coq/compose-installed-plugin.t/run.t

@@ -0,0 +1,15 @@
+Test for https://github.com/ocaml/dune/issues/7893
+When using an installed theory with plugins, things should work fine.
+
+  $ dune build --root to_install @all
+  Entering directory 'to_install'
+  Hello
+  Leaving directory 'to_install'
+  $ dune install --root to_install --prefix=$PWD
+
+We now build the normal theory, and should work
+
+  $ COQPATH=$PWD/lib/coq/user-contrib dune build --root user @all
+  Entering directory 'user'
+  Hello
+  Leaving directory 'user'

test/blackbox-tests/test-cases/coq/compose-installed-plugin.t/to_install/dune-project

@@ -0,0 +1,4 @@
+(lang dune 3.8)
+(using coq 0.8)
+
+(package (name global))

test/blackbox-tests/test-cases/coq/compose-installed-plugin.t/to_install/plugin/dune

@@ -0,0 +1,3 @@
+(library
+ (name plugin)
+ (public_name global.plugin))

test/blackbox-tests/test-cases/coq/compose-installed-plugin.t/to_install/plugin/p.ml

@@ -0,0 +1 @@
+let () = Format.eprintf "Hello@\n%!"

test/blackbox-tests/test-cases/coq/compose-installed-plugin.t/to_install/plugin/plugin.mlpack

@@ -0,0 +1 @@
+

test/blackbox-tests/test-cases/coq/compose-installed-plugin.t/to_install/theory/bar.v

@@ -0,0 +1 @@
+Declare ML Module "plugin:global.plugin".

test/blackbox-tests/test-cases/coq/compose-installed-plugin.t/to_install/theory/dune

@@ -0,0 +1,4 @@
+(coq.theory
+ (name Bar)
+ (package global)
+ (plugins global.plugin))

test/blackbox-tests/test-cases/coq/compose-installed-plugin.t/user/bar.v

@@ -0,0 +1 @@
+From Bar Require Import bar.

test/blackbox-tests/test-cases/coq/compose-installed-plugin.t/user/dune

@@ -0,0 +1,4 @@
+(coq.theory
+ (name Foo)
+ (package local)
+ (theories Bar))

test/blackbox-tests/test-cases/coq/compose-installed-plugin.t/user/dune-project

@@ -0,0 +1,4 @@
+(lang dune 3.8)
+(using coq 0.8)
+
+(package (name local))