Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[coq] Add .vos support #4050

Closed
wants to merge 2 commits into from
Closed

[coq] Add .vos support #4050

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4c69a94
[coq] Add .vos support
rgrinberg Dec 20, 2020
07db22e
do not install .vos files
rgrinberg Mar 8, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 7 additions & 2 deletions src/dune_rules/coq_module.ml
View file
Open in desktop
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,7 +78,8 @@ 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" ]
| Build Vo -> [ x.name ^ ".vo"; "." ^ x.name ^ ".aux"; x.name ^ ".glob" ]
| Build Vos -> [ x.name ^ ".vos" ]
| Install -> [ x.name ^ ".vo" ]
in
List.map obj_files ~f:(fun fname ->
Expand Down
6 changes: 5 additions & 1 deletion src/dune_rules/coq_module.mli
View file
Open in desktop
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
Open in desktop
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" ]
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This needs to be conditional as to support Coq older than 8.11

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But we don't have a way to check the version of Coq. Perhaps it should be enabled explicitly in the project file? E.g. (coq.vos enable)

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can also say that (coq lang 0.4) is required and only 8.11 upwards is supported

; 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
7 changes: 7 additions & 0 deletions test/blackbox-tests/test-cases/coq/base-unsound.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
2 changes: 2 additions & 0 deletions test/blackbox-tests/test-cases/coq/base.t/run.t
View file
Open in desktop
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 Down
13 changes: 13 additions & 0 deletions test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,4 +24,17 @@
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 alias thy2/all
[1]
17 changes: 4 additions & 13 deletions test/blackbox-tests/test-cases/coq/extract.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
1 change: 1 addition & 0 deletions test/blackbox-tests/test-cases/coq/ml-lib.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 4 additions & 0 deletions test/blackbox-tests/test-cases/coq/rec-module.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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: [
Expand Down