Skip to content

Commit

Permalink
[coq] Add .vos support
Browse files Browse the repository at this point in the history 
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>
  • Loading branch information
@rgrinberg @ejgallego
rgrinberg authored and ejgallego committed Feb 14, 2021
1 parent 72b4af3 commit ab533dd
Show file tree
Hide file tree
Showing 4 changed files with 102 additions and 70 deletions.
11 changes: 8 additions & 3 deletions src/dune_rules/coq_module.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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))
Expand Down
6 changes: 5 additions & 1 deletion src/dune_rules/coq_module.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
151 changes: 85 additions & 66 deletions src/dune_rules/coq_rules.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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));
Expand All @@ -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 =
Expand Down Expand Up @@ -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 *)
Expand Down Expand Up @@ -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
4 changes: 4 additions & 0 deletions test/blackbox-tests/test-cases/coq/base.t/run.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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: [
Expand All @@ -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"}
]

0 comments on commit ab533dd

Please sign in to comment.