coqdep -modules

[SkySkimmer]

In order to avoid having coqdep calls depend on all file contents, it would be useful to have a way to use coqdep like ocaml -modules.

This has 2 steps:

• make coqdep output the right stuff
• make dune use it

We need an output format for coqdep which can handle

• Declare ML Module "foo" "bar" (dependency on some cmxs)
• Require foo bar.baz and From x Require foo bar.baz (dependency on .vo)
• Load foo.bar and Load "foo" (dependency on .v)

coqdep also handles Add LoadPath but I don't think we want to support that.

[ejgallego]

See also coq/coq#12108

[ejgallego]

@SkySkimmer we can also use implement this #5457 (comment) , should be a one liner, let me try.

[ejgallego]

@Alizter has been working on this.

[Alizter]

So to elaborate further, I have a little binary called coqmod which is coqdep with all the useless stuff ripped out. It simply lexes the dependency tokens in a file and reports them. We can add a function to dune to interpret these.

https://github.com/Alizter/coq/tree/coqmod

[ejgallego]

This should also help solving #3286

[Alizter]

To sum up the status of this. I have implemented a prototype that lexes .v files for dependencies (let's call that coqmod). We can eventually upstream that. The question of what to do with with the tokens is however quite difficult.

In my prototype, I tried to follow the implementation of Coq's loadpath as closely as possible, and it appeared to work for most cases. The main issues I see here are that the loadpath specifications of Coq could probably be improved. For example to allow for ambiguous Require's with a clear preference order. This is however not something I want to touch atm.

The main advantage of this proposal would be the speed up by not having to call coqdep. In reality, once coqdep is called once per theory #7048, this not longer becomes the bottleneck during coq builds. The main bottleneck is the Coq compiler itself.