[coq] Ignore contents in coqdep rule

[ejgallego]

This should help reduce the coqdep calls drastically.

Improves #5100 .

In particular, while a build from scratch has still one coqdep call per file overhead, incremental builds don't anymore. This makes one coqdep call per theory (or -modules) much less critical.

[rgrinberg]

Doesn't coqdep read these files? If so, then this optimization isn't correct.

[ejgallego]

Doesn't coqdep read these files? If so, then this optimization isn't correct.

No, it doesn't read them, they are only used because Coq has no -modules.

[Alizter]

I am also puzzled here. What happens if I add extra Requires in a .v file, since the file system hasn't been updated, wouldn't coqdep need to be called again?

[ejgallego]

@Alizter only for that file, as shown in the test.

[ejgallego]

@Alizter only for that file, as shown in the test.

In particular, note that that coqdep_rule has:

  let file_flags =
    [ Command.Args.S file_flags
    ; As [ "-dyndep"; "opt" ]
    ; Dep (Path.build source)
    ]
  in
  let stdout_to = Coq_module.dep_file ~obj_dir:cctx.dir coq_module in
  (* Coqdep has to be called in the stanza's directory *)
  let open Action_builder.With_targets.O in
  Action_builder.with_no_targets cctx.mlpack_rule
  >>> Action_builder.(with_no_targets (goal source_rule))
  >>> Command.run ~dir:(Path.build cctx.dir) ~stdout_to cctx.coqdep file_flags

so Dep (Path.build source) forces the rule to rerun when the .v file changes.

[Blaisorblade]

This is great and works indeed as intended!

[ejgallego]

It must been annoying to work with dune before this PR @Blaisorblade !

We still have plenty of low-hanging fruit to reap.