Skip to content

Commit

Permalink
refactor(coq): make hint in resolve_program optional
Browse files Browse the repository at this point in the history
We also pattern match the coqpp stanza since it is simple.

Signed-off-by: Ali Caglayan <[email protected]>

ps-id: 92836235-2b74-4a26-8f68-ebe3674ec415
  • Loading branch information
Alizter authored and ejgallego committed Oct 10, 2022
1 parent a801d29 commit 3a999b8
Showing 1 changed file with 5 additions and 7 deletions.
12 changes: 5 additions & 7 deletions src/dune_rules/coq_rules.ml
Original file line number Diff line number Diff line change
Expand Up @@ -51,9 +51,8 @@ module Util = struct
]
end

let resolve_program sctx ~loc ~dir prog =
Super_context.resolve_program ~dir sctx prog ~loc:(Some loc)
~hint:"opam install coq"
let resolve_program sctx ~loc ~dir ?(hint = "opam install coq") prog =
Super_context.resolve_program ~dir sctx prog ~loc:(Some loc) ~hint

module Coq_plugin = struct
(* compute include flags and mlpack rules *)
Expand Down Expand Up @@ -703,17 +702,16 @@ let install_rules ~sctx ~dir s =
make_entry vfile vfile_dst :: obj_files)
|> List.rev_append coq_plugins_install_rules

let setup_coqpp_rules ~sctx ~dir (s : Coqpp.t) =
let* coqpp = resolve_program sctx ~dir ~loc:s.loc "coqpp" in
let setup_coqpp_rules ~sctx ~dir ({ loc; modules } : Coqpp.t) =
let* coqpp = resolve_program sctx ~dir ~loc "coqpp" in
let mlg_rule m =
let source = Path.build (Path.Build.relative dir (m ^ ".mlg")) in
let target = Path.Build.relative dir (m ^ ".ml") in
let args = [ Command.Args.Dep source; Hidden_targets [ target ] ] in
let build_dir = (Super_context.context sctx).build_dir in
Command.run ~dir:(Path.build build_dir) coqpp args
in
List.rev_map ~f:mlg_rule s.modules
|> Super_context.add_rules ~loc:s.loc ~dir sctx
List.rev_map ~f:mlg_rule modules |> Super_context.add_rules ~loc ~dir sctx

let setup_extraction_cctx_and_modules ~sctx ~dir ~dir_contents
(s : Extraction.t) =
Expand Down

0 comments on commit 3a999b8

Please sign in to comment.