search

lukaszcz / coqhammer

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

Build from source fails #137

Closed will-leeson closed 2 years ago

will-leeson commented 2 years ago

When running make in the root directory, I get several errors like the following

COQDEP VFILES *** Error: in file theories/Tactics/Tactics.v, hammer_lib is not a valid plugin name anymore.Plugins should be loaded using their public name according to findlib, for example package-name.foo and not foo_plugin. If you are using a buid system that doesn't yet support the new loading method (such as Dune) you must specify both the legacy and the findlib plugin name as in: Declare ML Module "foo_plugin:package-name.foo".

I've attempted to fix them by changing Declare ML Module "hammer_lib". to Declare ML Module "hammer_lib:g_hammer_lib.hammer". but then I get the follwoing error

File "src/lib/g_hammer_lib.mlg", line 17, characters 26-48: Error: The function applied to this argument has type ?info:Exninfo.info -> 'a Proofview.tactic This argument cannot be applied without label

I am very new to coq and OCaml, so I'm not sure the way I fixed the first error was correct. Any help would be appreciated

coqtop --version returned: The Coq Proof Assistant, version 8.17+alpha compiled with OCaml 4.12.0

lukaszcz commented 2 years ago

You're using Coq 8.17+alpha. Which CoqHammer branch did you use? It should work with master. If not, try using the latest supported non-alpha version of Coq: 8.15. Coq sources change all the time. I have no idea what's going on there, except that the CoqHammer version does not match your Coq version.