Skip to content

Commit

Permalink
[coq] Ignore contents in coqdep rule
Browse files Browse the repository at this point in the history
This should help reduce the coqdep calls drastically.

Improves ocaml#5100 .
  • Loading branch information
ejgallego committed Apr 5, 2022
1 parent 4bc7629 commit ca7e735
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 1 deletion.
3 changes: 3 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,9 @@
- Fix operations that remove folders with absolute path. This happens when
using esy (#5507, @EduardoRFS)

- `coqdep` now depends only on the filesystem layout of the .v files,
and not on their contents (#XXXX , helps with #5100 , @ejgallego)

3.0.3 (Unreleased)
------------------

Expand Down
2 changes: 1 addition & 1 deletion src/dune_rules/coq_rules.ml
Original file line number Diff line number Diff line change
Expand Up @@ -566,7 +566,7 @@ let extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) =
let source_rule =
let theories = source_rule ~sctx cctx.theories_deps in
let open Action_builder.O in
theories >>> Action_builder.path (Path.build (Coq_module.source coq_module))
theories >>> Action_builder.(goal (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 ~file_targets:ml_targets in
Expand Down

0 comments on commit ca7e735

Please sign in to comment.