From 4c69a9442744ba6bd55c3122ca4af727baf6b86d Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Sat, 19 Dec 2020 20:58:53 -0800 Subject: [PATCH] [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 --- src/dune_rules/coq_module.ml | 11 +- src/dune_rules/coq_module.mli | 6 +- src/dune_rules/coq_rules.ml | 151 ++++++++++-------- .../test-cases/coq/base-unsound.t/run.t | 7 + .../test-cases/coq/base.t/run.t | 4 + .../test-cases/coq/compose-plugin.t/run.t | 15 ++ .../test-cases/coq/compose-simple.t/run.t | 21 ++- .../test-cases/coq/compose-sub-theory.t/run.t | 21 ++- .../test-cases/coq/extract.t/run.t | 17 +- .../test-cases/coq/ml-lib.t/run.t | 1 + .../test-cases/coq/rec-module.t/run.t | 8 + 11 files changed, 157 insertions(+), 105 deletions(-) diff --git a/src/dune_rules/coq_module.ml b/src/dune_rules/coq_module.ml index 3d944b1c07a..282b3ea84f8 100644 --- a/src/dune_rules/coq_module.ml +++ b/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)) diff --git a/src/dune_rules/coq_module.mli b/src/dune_rules/coq_module.mli index 5c48f061c71..85c289c88db 100644 --- a/src/dune_rules/coq_module.mli +++ b/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 diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml index 2d3bd2e4688..f2fbfdf8720 100644 --- a/src/dune_rules/coq_rules.ml +++ b/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 diff --git a/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t b/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t index 4d7f98a4952..472fcbf9d47 100644 --- a/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t +++ b/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] diff --git a/test/blackbox-tests/test-cases/coq/base.t/run.t b/test/blackbox-tests/test-cases/coq/base.t/run.t index 8ac016d27fe..83b5883a97e 100644 --- a/test/blackbox-tests/test-cases/coq/base.t/run.t +++ b/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"} ] diff --git a/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t b/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t index 78b691f2922..586ba03a044 100644 --- a/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t +++ b/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] diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t b/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t index d1626e74578..0f8614683ca 100644 --- a/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t +++ b/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] diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t index 8f1321b1291..e5edb4e51f0 100644 --- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t +++ b/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] diff --git a/test/blackbox-tests/test-cases/coq/extract.t/run.t b/test/blackbox-tests/test-cases/coq/extract.t/run.t index 42405dd01d5..3f9ef6fe2d4 100644 --- a/test/blackbox-tests/test-cases/coq/extract.t/run.t +++ b/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: + - + - + [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 diff --git a/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t b/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t index 0f8a193571c..a31df61854c 100644 --- a/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t +++ b/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 diff --git a/test/blackbox-tests/test-cases/coq/rec-module.t/run.t b/test/blackbox-tests/test-cases/coq/rec-module.t/run.t index 99fba5a0cc9..5d8a4f071c3 100644 --- a/test/blackbox-tests/test-cases/coq/rec-module.t/run.t +++ b/test/blackbox-tests/test-cases/coq/rec-module.t/run.t @@ -4,9 +4,13 @@ coqdep c/d/bar.v.d coqdep c/ooo.v.d coqc b/.foo.aux,b/foo.{glob,vo} + coqc b/foo.vos coqc c/d/.bar.aux,c/d/bar.{glob,vo} + coqc c/d/bar.vos coqc c/.ooo.aux,c/ooo.{glob,vo} + coqc c/ooo.vos coqc a/.bar.aux,a/bar.{glob,vo} + coqc a/bar.vos $ dune build --debug-dependency-path @default lib: [ @@ -17,10 +21,14 @@ lib_root: [ "_build/install/default/lib/coq/user-contrib/rec_module/a/bar.v" {"coq/user-contrib/rec_module/a/bar.v"} "_build/install/default/lib/coq/user-contrib/rec_module/a/bar.vo" {"coq/user-contrib/rec_module/a/bar.vo"} + "_build/install/default/lib/coq/user-contrib/rec_module/a/bar.vos" {"coq/user-contrib/rec_module/a/bar.vos"} "_build/install/default/lib/coq/user-contrib/rec_module/b/foo.v" {"coq/user-contrib/rec_module/b/foo.v"} "_build/install/default/lib/coq/user-contrib/rec_module/b/foo.vo" {"coq/user-contrib/rec_module/b/foo.vo"} + "_build/install/default/lib/coq/user-contrib/rec_module/b/foo.vos" {"coq/user-contrib/rec_module/b/foo.vos"} "_build/install/default/lib/coq/user-contrib/rec_module/c/d/bar.v" {"coq/user-contrib/rec_module/c/d/bar.v"} "_build/install/default/lib/coq/user-contrib/rec_module/c/d/bar.vo" {"coq/user-contrib/rec_module/c/d/bar.vo"} + "_build/install/default/lib/coq/user-contrib/rec_module/c/d/bar.vos" {"coq/user-contrib/rec_module/c/d/bar.vos"} "_build/install/default/lib/coq/user-contrib/rec_module/c/ooo.v" {"coq/user-contrib/rec_module/c/ooo.v"} "_build/install/default/lib/coq/user-contrib/rec_module/c/ooo.vo" {"coq/user-contrib/rec_module/c/ooo.vo"} + "_build/install/default/lib/coq/user-contrib/rec_module/c/ooo.vos" {"coq/user-contrib/rec_module/c/ooo.vos"} ]