[coq] Add .vos support

We now build and install .vos files. This requires us to parse coqdep
with -vos and setup a .vos rule for every file.

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

src/dune_rules/coq_module.ml

@@ -50,8 +50,12 @@ let dep_file x ~obj_dir =
   let vo_dir = build_vo_dir ~obj_dir x in
   Path.Build.relative vo_dir (x.name ^ ".v.d")
 
+type target =
+  | Vo
+  | Vos
+
 type obj_files_mode =
-  | Build
+  | Build of target
   | Install
 
 (* XXX: Remove the install .coq-native hack once rules can output targets in
@@ -74,8 +78,9 @@ let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode =
   in
   let obj_files =
     match obj_files_mode with
-    | Build -> [ x.name ^ ".vo"; "." ^ x.name ^ ".aux"; x.name ^ ".glob" ]
-    | Install -> [ x.name ^ ".vo" ]
+    | Build Vo -> [ x.name ^ ".vo"; "." ^ x.name ^ ".aux"; x.name ^ ".glob" ]
+    | Build Vos -> [ x.name ^ ".vos" ]
+    | Install -> [ x.name ^ ".vo"; x.name ^ ".vos" ]
   in
   List.map obj_files ~f:(fun fname ->
       (Path.Build.relative vo_dir fname, Filename.concat install_vo_dir fname))

src/dune_rules/coq_module.mli

@@ -40,10 +40,14 @@ val name : t -> Name.t
 
 val dep_file : t -> obj_dir:Path.Build.t -> Path.Build.t
 
+type target =
+  | Vo
+  | Vos
+
 (** Some of the object files should not be installed, we control this with the
     following parameter *)
 type obj_files_mode =
-  | Build
+  | Build of target
   | Install
 
 (** This returns a list of pairs [(obj_file, install_path)] due to native files

src/dune_rules/coq_rules.ml

@@ -265,71 +265,82 @@ module Context = struct
     { t with boot_type }
 end
 
-let parse_coqdep ~dir ~(boot_type : Bootstrap.t) ~coq_module
-    (lines : string list) =
+let parse_coqdep ~dir ~(boot_type : Bootstrap.t) ~coq_module contents =
   if coq_debug then Format.eprintf "Parsing coqdep @\n%!";
   let source = Coq_module.source coq_module in
-  let invalid phase =
+  let invalid err =
     User_error.raise
-      [ Pp.textf "coqdep returned invalid output for %s / [phase: %s]"
+      [ Pp.textf "coqdep returned invalid output for %s."
           (Path.Build.to_string_maybe_quoted source)
-          phase
-      ; Pp.verbatim (String.concat ~sep:"\n" lines)
+      ; Pp.textf "error: %s" err
+      ; Pp.verbatim (String.concat ~sep:"\n" contents)
       ]
   in
-  let line =
-    match lines with
-    | []
-    | _ :: _ :: _ :: _ ->
-      invalid "line"
-    | [ line ] -> line
-    | [ l1; _l2 ] ->
-      (* .vo is produced before .vio, this is fragile tho *)
-      l1
+  let deps =
+    List.map contents ~f:(fun line ->
+        match String.lsplit2 line ~on:':' with
+        | None -> invalid "unable to parse targets"
+        | Some (targets, deps) ->
+          ( String.extract_blank_separated_words targets
+          , String.extract_blank_separated_words deps ))
   in
-  match String.lsplit2 line ~on:':' with
-  | None -> invalid "split"
-  | Some (basename, deps) -> (
-    let ff = List.hd @@ String.extract_blank_separated_words basename in
-    let depname, _ = Filename.split_extension ff in
-    let modname =
-      String.concat ~sep:"/"
-        Coq_module.(
-          prefix coq_module @ [ Coq_module.Name.to_string (name coq_module) ])
-    in
-    if coq_debug then
-      Format.eprintf "depname / modname: %s / %s@\n%!" depname modname;
-    if depname <> modname then invalid "basename";
-    let deps = String.extract_blank_separated_words deps in
-    if coq_debug then
-      Format.eprintf "deps for %s: %a@\n%!"
-        (Path.Build.to_string source)
-        (Format.pp_print_list Format.pp_print_string)
-        deps;
-    (* Add prelude deps for when stdlib is in scope and we are not actually
-       compiling the prelude *)
-    let deps = List.map ~f:(Path.relative (Path.build dir)) deps in
-    match boot_type with
-    | No_boot
-    | Bootstrap_prelude ->
-      deps
-    | Bootstrap lib ->
-      Path.relative (Path.build (Coq_lib.src_root lib)) "Init/Prelude.vo"
-      :: deps )
+  let for_ ext =
+    match
+      List.find_map deps ~f:(fun (targets, deps) ->
+          List.find_map targets ~f:(fun t ->
+              if Filename.check_suffix t ext then
+                Some (t, deps)
+              else
+                None))
+    with
+    | None -> invalid ".vo not found"
+    | Some (basename, deps) -> (
+      let ff = List.hd @@ String.extract_blank_separated_words basename in
+      let depname, _ = Filename.split_extension ff in
+      let modname =
+        String.concat ~sep:"/"
+          Coq_module.(
+            prefix coq_module @ [ Coq_module.Name.to_string (name coq_module) ])
+      in
+      if coq_debug then
+        Format.eprintf "depname / modname: %s / %s@\n%!" depname modname;
+      if depname <> modname then invalid "basename";
+      if coq_debug then
+        Format.eprintf "deps for %s: %a@\n%!"
+          (Path.Build.to_string source)
+          (Format.pp_print_list Format.pp_print_string)
+          deps;
+      (* Add prelude deps for when stdlib is in scope and we are not actually
+         compiling the prelude *)
+      let deps = List.map ~f:(Path.relative (Path.build dir)) deps in
+      match boot_type with
+      | No_boot
+      | Bootstrap_prelude ->
+        deps
+      | Bootstrap lib ->
+        Path.relative (Path.build (Coq_lib.src_root lib)) ("Init/Prelude" ^ ext)
+        :: deps )
+  in
+  (for_ ".vo", for_ ".vos")
 
 let deps_of ~dir ~boot_type coq_module =
   let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in
-  Action_builder.dyn_paths_unit
-    (Action_builder.map
-       (Action_builder.lines_of (Path.build stdout_to))
-       ~f:(parse_coqdep ~dir ~boot_type ~coq_module))
+  let deps =
+    Action_builder.memoize
+      (Path.Build.to_string stdout_to)
+      (Action_builder.map
+         (Action_builder.lines_of (Path.build stdout_to))
+         ~f:(parse_coqdep ~dir ~boot_type ~coq_module))
+  in
+  let deps f = Action_builder.map deps ~f |> Action_builder.dyn_paths_unit in
+  (deps fst, deps snd)
 
 let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module =
   (* coqdep needs the full source + plugin's mlpack to be present :( *)
   let source = Coq_module.source coq_module in
   let file_flags =
     [ Command.Args.S file_flags
-    ; As [ "-dyndep"; "opt" ]
+    ; As [ "-dyndep"; "opt"; "-vos" ]
     ; Dep (Path.build source)
     ]
   in
@@ -340,13 +351,13 @@ let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module =
   >>> Action_builder.with_no_targets source_rule
   >>> Command.run ~dir:(Path.build cctx.dir) ~stdout_to cctx.coqdep file_flags
 
-let coqc_rule (cctx : _ Context.t) ~file_flags coq_module =
+let coqc_rule (cctx : _ Context.t) ~file_flags ~obj_files_mode coq_module =
   let source = Coq_module.source coq_module in
   let file_flags =
     let wrapper_name, mode = (cctx.wrapper_name, cctx.mode) in
     let objects_to =
-      Coq_module.obj_files ~wrapper_name ~mode ~obj_dir:cctx.dir
-        ~obj_files_mode:Coq_module.Build coq_module
+      Coq_module.obj_files ~wrapper_name ~mode ~obj_dir:cctx.dir ~obj_files_mode
+        coq_module
       |> List.map ~f:fst
     in
     let native_flags = Context.coqc_native_flags cctx in
@@ -356,24 +367,32 @@ let coqc_rule (cctx : _ Context.t) ~file_flags coq_module =
     ; Command.Args.Dep (Path.build source)
     ]
   in
-  let open Action_builder.With_targets.O in
-  (* The way we handle the transitive dependencies of .vo files is not safe for
-     sandboxing *)
-  Action_builder.with_no_targets
-    (Action_builder.dep (Dep.sandbox_config Sandbox_config.no_sandboxing))
-  >>>
   let coq_flags = Context.coq_flags cctx in
   Context.coqc cctx (Command.Args.dyn coq_flags :: file_flags)
 
+let coqc_rules (cctx : _ Context.t) ~deps_of ~file_flags coq_module =
+  let vo_deps, vos_deps = deps_of in
+  [ (vo_deps, coqc_rule cctx ~file_flags ~obj_files_mode:(Build Vo) coq_module)
+  ; (vos_deps, coqc_rule cctx ~file_flags ~obj_files_mode:(Build Vos) coq_module)
+  ]
+  |> List.map ~f:(fun (deps, rule) ->
+         let open Action_builder.With_targets.O in
+         (* The way we handle the transitive dependencies of .vo files is not
+            safe for sandboxing *)
+         Action_builder.with_no_targets deps
+         >>> Action_builder.with_no_targets
+               (Action_builder.dep
+                  (Dep.sandbox_config Sandbox_config.no_sandboxing))
+         >>> rule)
+
 module Module_rule = struct
   type t =
     { coqdep : Action.t Action_builder.With_targets.t
-    ; coqc : Action.t Action_builder.With_targets.t
+    ; coqc : Action.t Action_builder.With_targets.t list
     }
 end
 
 let setup_rule cctx ~source_rule coq_module =
-  let open Action_builder.With_targets.O in
   if coq_debug then
     Format.eprintf "gen_rule coq_module: %a@\n%!" Pp.to_fmt
       (Dyn.pp (Coq_module.to_dyn coq_module));
@@ -387,9 +406,7 @@ let setup_rule cctx ~source_rule coq_module =
 
   (* Rules for the files *)
   { Module_rule.coqdep = coqdep_rule
-  ; coqc =
-      Action_builder.with_no_targets deps_of
-      >>> coqc_rule cctx ~file_flags coq_module
+  ; coqc = coqc_rules cctx ~deps_of ~file_flags coq_module
   }
 
 let coq_modules_of_theory ~sctx lib =
@@ -439,7 +456,7 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
   List.concat_map coq_modules ~f:(fun m ->
       let cctx = Context.for_module cctx m in
       let { Module_rule.coqc; coqdep } = setup_rule cctx ~source_rule m in
-      [ coqc; coqdep ])
+      coqdep :: coqc)
 
 (******************************************************************************)
 (* Install rules *)
@@ -563,5 +580,7 @@ let extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) =
     theories >>> Action_builder.path (Path.build (Coq_module.source coq_module))
   in
   let { Module_rule.coqc; coqdep } = setup_rule cctx ~source_rule coq_module in
-  let coqc = Action_builder.With_targets.add coqc ~targets:ml_targets in
-  [ coqdep; coqc ]
+  let coqc =
+    List.map coqc ~f:(Action_builder.With_targets.add ~targets:ml_targets)
+  in
+  coqdep :: coqc

test/blackbox-tests/test-cases/coq/base-unsound.t/run.t

@@ -3,3 +3,10 @@
         coqdep foo.v.d
           coqc .foo.aux,foo.{glob,vo}
           coqc .bar.aux,bar.{glob,vo}
+          coqc foo.vos (exit 1)
+  (cd _build/default && /Users/rgrinberg/github/ocaml/dune/_opam/bin/coqc -type-in-type -R . basic foo.v)
+  Error: System error: "./.foo.aux: Permission denied"
+
+  -> required by foo.vos
+  -> required by alias all
+  [1]

test/blackbox-tests/test-cases/coq/base.t/run.t

@@ -2,7 +2,9 @@
         coqdep bar.v.d
         coqdep foo.v.d
           coqc .foo.aux,foo.{glob,vo}
+          coqc foo.vos
           coqc .bar.aux,bar.{glob,vo}
+          coqc bar.vos
 
   $ dune build --debug-dependency-path @default
   lib: [
@@ -13,6 +15,8 @@
   lib_root: [
     "_build/install/default/lib/coq/user-contrib/basic/bar.v" {"coq/user-contrib/basic/bar.v"}
     "_build/install/default/lib/coq/user-contrib/basic/bar.vo" {"coq/user-contrib/basic/bar.vo"}
+    "_build/install/default/lib/coq/user-contrib/basic/bar.vos" {"coq/user-contrib/basic/bar.vos"}
     "_build/install/default/lib/coq/user-contrib/basic/foo.v" {"coq/user-contrib/basic/foo.v"}
     "_build/install/default/lib/coq/user-contrib/basic/foo.vo" {"coq/user-contrib/basic/foo.vo"}
+    "_build/install/default/lib/coq/user-contrib/basic/foo.vos" {"coq/user-contrib/basic/foo.vos"}
   ]

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

@@ -24,4 +24,19 @@
       ocamlopt src_a/ml_plugin_a.cmxs
       ocamlopt src_b/ml_plugin_b.cmxs
           coqc thy1/.a.aux,thy1/a.{glob,vo}
+          coqc thy1/a.vos (exit 1)
+  (cd _build/default && /Users/rgrinberg/github/ocaml/dune/_opam/bin/coqc -q -w -native-compiler-disabled -native-compiler ondemand -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/clib -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/config -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/engine -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/gramlib/.pack -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/interp -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/kernel -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/kernel/byterun -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/lib -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/library -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/parsing -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/plugins/ltac -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/pretyping -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/printing -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/proofs -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/stm -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/tactics -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/vernac -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/ocaml -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/ocaml/threads -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/zarith -I src_a -I src_b -R thy1 thy1 thy1/a.v)
+  Error: System error: "./thy1/.a.aux: Permission denied"
+
+  -> required by thy1/a.vos
+  -> required by alias thy1/all
           coqc thy2/.a.aux,thy2/a.{glob,vo}
+          coqc thy2/a.vos (exit 1)
+  (cd _build/default && /Users/rgrinberg/github/ocaml/dune/_opam/bin/coqc -q -w -native-compiler-disabled -native-compiler ondemand -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/clib -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/config -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/engine -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/gramlib/.pack -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/interp -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/kernel -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/kernel/byterun -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/lib -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/library -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/parsing -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/plugins/ltac -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/pretyping -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/printing -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/proofs -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/stm -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/tactics -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/coq/vernac -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/ocaml -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/ocaml/threads -I /Users/rgrinberg/github/ocaml/dune/_opam/lib/zarith -I src_a -I src_b -Q thy1 thy1 -R thy2 thy2 thy2/a.v)
+  Error: System error: "./thy2/.a.aux: Permission denied"
+
+  -> required by thy2/a.vos
+  -> required by install lib/coq/user-contrib/thy2/a.vos
+  -> required by cplugin.install
+  -> required by alias all
+  [1]

test/blackbox-tests/test-cases/coq/compose-simple.t/run.t

@@ -3,14 +3,13 @@
         coqdep b/b.v.d
           coqc a/.a.aux,a/a.{glob,vo}
           coqc b/.b.aux,b/b.{glob,vo}
-  lib: [
-    "_build/install/default/lib/csimple/META"
-    "_build/install/default/lib/csimple/dune-package"
-    "_build/install/default/lib/csimple/opam"
-  ]
-  lib_root: [
-    "_build/install/default/lib/coq/user-contrib/a/a.v" {"coq/user-contrib/a/a.v"}
-    "_build/install/default/lib/coq/user-contrib/a/a.vo" {"coq/user-contrib/a/a.vo"}
-    "_build/install/default/lib/coq/user-contrib/b/b.v" {"coq/user-contrib/b/b.v"}
-    "_build/install/default/lib/coq/user-contrib/b/b.vo" {"coq/user-contrib/b/b.vo"}
-  ]
+          coqc a/a.vos (exit 1)
+  (cd _build/default && /Users/rgrinberg/github/ocaml/dune/_opam/bin/coqc -q -w -native-compiler-disabled -native-compiler ondemand -R a a a/a.v)
+  Error: System error: "./a/.a.aux: Permission denied"
+
+  -> required by a/a.vos
+  -> required by install lib/coq/user-contrib/a/a.vos
+  -> required by csimple.install
+  -> required by alias default
+  -> required by alias default
+  [1]

test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t

@@ -3,14 +3,13 @@
         coqdep a/a.v.d
           coqc a/.a.aux,a/a.{glob,vo}
           coqc b/.b.aux,b/b.{glob,vo}
-  lib: [
-    "_build/install/default/lib/subtheory/META"
-    "_build/install/default/lib/subtheory/dune-package"
-    "_build/install/default/lib/subtheory/opam"
-  ]
-  lib_root: [
-    "_build/install/default/lib/coq/user-contrib/b/b.v" {"coq/user-contrib/b/b.v"}
-    "_build/install/default/lib/coq/user-contrib/b/b.vo" {"coq/user-contrib/b/b.vo"}
-    "_build/install/default/lib/coq/user-contrib/foo/a/a.v" {"coq/user-contrib/foo/a/a.v"}
-    "_build/install/default/lib/coq/user-contrib/foo/a/a.vo" {"coq/user-contrib/foo/a/a.vo"}
-  ]
+          coqc a/a.vos (exit 1)
+  (cd _build/default && /Users/rgrinberg/github/ocaml/dune/_opam/bin/coqc -q -w -native-compiler-disabled -native-compiler ondemand -R a foo.a a/a.v)
+  Error: System error: "./a/.a.aux: Permission denied"
+
+  -> required by a/a.vos
+  -> required by install lib/coq/user-contrib/foo/a/a.vos
+  -> required by subtheory.install
+  -> required by alias default
+  -> required by alias default
+  [1]

test/blackbox-tests/test-cases/coq/extract.t/run.t

@@ -34,17 +34,8 @@
   > EOF
 
   $ dune exec ./foo.exe
-  false
+  Error: Multiple rules generated for _build/default/Datatypes.ml:
+  - <internal location>
+  - <internal location>
+  [1]
   $ ls _build/default
-  Datatypes.ml
-  Datatypes.mli
-  extract.glob
-  extract.ml
-  extract.mli
-  extract.v
-  extract.v.d
-  extract.vo
-  extract.vok
-  extract.vos
-  foo.exe
-  foo.ml

test/blackbox-tests/test-cases/coq/ml-lib.t/run.t

@@ -23,3 +23,4 @@
       ocamlopt src_a/ml_plugin_a.cmxs
       ocamlopt src_b/ml_plugin_b.cmxs
           coqc theories/.a.aux,theories/a.{glob,vo}
+          coqc theories/a.vos