Skip to content

Commit

Permalink
[coq] Memoize coqdep parsing
Browse files Browse the repository at this point in the history
I was under the impression that our current code was taking care of
this already, however it was not.

Suggestions on what is best w.r.t. `Memo/Action_builder` code dance welcome.

Obviously, this has a dramatic effect on most Coq builds, for example
HoTT's zero build is now:

```
before:
-------

real	0m5,302s
user	0m5,197s
sys	0m0,056s

after:
------

real	0m0,210s
user	0m0,143s
sys	0m0,034s
```

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
  • Loading branch information
ejgallego committed Feb 22, 2024
1 parent b5a4f6a commit adf8dee
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 1 deletion.
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)
19 changes: 18 additions & 1 deletion src/dune_rules/coq/coq_rules.ml
Original file line number Diff line number Diff line change
Expand Up @@ -550,6 +550,7 @@ let parse_line ~dir line =
;;

let get_dep_map ~dir ~wrapper_name : Path.t list Dep_map.t Action_builder.t =
Format.eprintf "[get_dep_map: %s %s]@\n" (Path.Build.to_string dir) wrapper_name;
let file = dep_theory_file ~dir ~wrapper_name in
let open Action_builder.O in
let f = parse_line ~dir in
Expand All @@ -569,6 +570,22 @@ let get_dep_map ~dir ~wrapper_name : Path.t list Dep_map.t Action_builder.t =
]
;;

module DirWrapper = 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: Should we instead use Action_builder.memoize ? *)
let memo_get_dep_map =
Action_builder.create_memo
"coq_dep_map"
~input:(module DirWrapper)
(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 @@ -579,7 +596,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

0 comments on commit adf8dee

Please sign in to comment.