Dune build error

[lukaszcz]

I run "dune build" and get the following error:

  coqdep theories/Plugin/Hammer.v.d

*** Warning: in file Hammer.v, library Hammer.Tactics.Tactics is required and has not been found in the loadpath!
File "./theories/Plugin/Hammer.v", line 1, characters 27-42:
Error: Unable to locate library Tactics.Tactics with prefix Hammer.

I notice that uncommenting the line

;(theories Hammer.Tactics)

in the file theories/Plugin/dune solves the problem. But I don't know what the purpose of commenting the line out was and whether it won't affect something else.

[palmskog]

This is a current limitation of Dune support for Coq. We have to make a choice between:

1. supporting the case where Dune is used to build and install coq-hammer-tactics and coq-hammer in turn via dune build -p <package> && dune install, or
2. supporting builds of the whole thing with dune build && dune install.

I chose the first option, which is why (theories Hammer.Tactics) is commented out. We can't support both cases simultaneously until Dune 2.8 or so.

[lukaszcz]

OK, so let's leave it as it is for now