search

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
211 stars 31 forks source link

Dune build error #92

Open lukaszcz opened 3 years ago

lukaszcz commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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