Dune cannot handle `From ... Extra Dependency`

[Blaisorblade]

Expected Behavior

Dune can build a cast.v file containing From elpi.apps.derive Extra Dependency "cast.elpi" as cast.

Actual Behavior

Building cast.v.d doesn't work as expected, because cast.elpi wasn't copied to the target directory; IIRC it appears the coqdep tasks only depend on copying .v files. Disclaimer: I looked at this with @swasey a couple of weeks ago on dune 3.6, but we should retest, probably with the new coqdep setup.

At least, dune could let us declare explicitly .elpi files to depend on — a bit like #7056. cc @Alizter @ejgallego .

[ejgallego]

It is indeed unfortunate that we must compute the set of source files before calling coqdep; I think we had an issue for this already open.

The idea was to add a field to a Coq theory (extra_sources ...) which are then just passed to the source_rule setup in Coq_rules.

I don't see any challenge implementing this.

[ejgallego]

But yes, no need to test with the new setup, Dune will just not place the file on the source tree, as it computes the list of modules from .v files exclusively.

You can inject the dep with a hack tho for now: generate an empty source file foo.v with a rule, make that rule depend on the elpi files.

[Blaisorblade]

Thanks for the prompt answer, and that work around sounds great!

Would extra_sources have any overlap with #7056? It seems extra_sources could also fix #3286 — said otherwise, if you had extra_sources already, would you still support (load_only mCoefStructure.v) instead of suggesting

(modules :standard \ mCoefStructure)
(extra_sources mCoefStructure.v)

I'm not trying to push this option, just checking if you'd prefer a combined design.

[Alizter]

@Blaisorblade I don't think this overlaps with #7056 since in that case, coqdep is also run on the .v files that we load.

[ejgallego]

Indeed the idea of having a simpler system as @Blaisorblade 's proposes seems attractive to me.

It is true that we would lose the ability to run coqdep on the file, or we would have to scan the extra_deps file for .vo files; so I dunno.

[Blaisorblade]

@Alizter I'm afraid I don't follow — since Load is almost just #include*, why would you run coqdep also on the loaded file? Running it on the loading file seems enough, since it includes all deps.

I could be wrong (I never use Load) but I ran a quick test: with Load load1 in load2.v we don't need coqdep load1.v or coqc load1.v, so I expect neither proposal would run coqdep; in fact, coqc load1.v can fail with syntax errors.

You just coqdep load2.v and coqc load2.v — coqdep's output will include load1's dependencies.

Here's the test. Beware it relies on . being in the loadpath — arguably I should have used folders: https://gist.github.com/Blaisorblade/7006fbaa5fcad0e14c70563c13b35c56

* IIUC from the docs

[Alizter]

@Blaisorblade nevermind you are correct. After going through coqdep sources, it turns out it handles the case I was worried about anyway. There doesn't seem to be anything stopping us from implementing both features the same way.

[gares]

The bug is still present in dune 3.12