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.

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] Memoize coqdep parsing #10116

Merged
merged 1 commit into from
Feb 22, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
3 changes: 3 additions & 0 deletions doc/changes/10116.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
- coq: memoize coqdep parsing, this will reduce build times for Coq
users, in particular for those with many .v files (#10116,
@ejgallego, see also #10088)
22 changes: 21 additions & 1 deletion src/dune_rules/coq/coq_rules.ml
Original file line number Diff line number Diff line change
Expand Up @@ -570,6 +570,26 @@ let get_dep_map ~dir ~wrapper_name : Path.t list Dep_map.t Action_builder.t =
]
;;

(* EJGA: Would be nice to have a functor in [Stdune.Tuple] to do this *)
module DWInput : Memo.Input with type t = Path.Build.t * string = struct
type t = Path.Build.t * string

let hash = Tuple.T2.hash Path.Build.hash String.hash
let equal = Tuple.T2.equal Path.Build.equal String.equal
let to_dyn = Tuple.T2.to_dyn Path.Build.to_dyn String.to_dyn
end

(* EJGA: with this code, we have a combined memo node that will be
re-executed iff [dir], [wrapper_name], or the deps of the original
action builder (the [.v.d] file from [dep_theory_file ~dir
~wrapper_name]) change *)
let memo_get_dep_map =
Action_builder.create_memo
"coq_dep_map"
~input:(module DWInput)
(fun (dir, wrapper_name) -> get_dep_map ~dir ~wrapper_name)
;;

let deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module =
let open Action_builder.O in
let vo_target =
Expand All @@ -580,7 +600,7 @@ let deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module =
in
Path.set_extension ~ext (Coq_module.source coq_module)
in
let* dep_map = get_dep_map ~dir ~wrapper_name in
let* dep_map = Action_builder.exec_memo memo_get_dep_map (dir, wrapper_name) in
let* boot_type = Resolve.Memo.read boot_type in
match Dep_map.find dep_map vo_target with
| None ->
Expand Down
Loading