search

lukaszcz / coqhammer

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

Trouble compiling 1.3.2+8.16 #147

Closed SnarkBoojum closed 2 years ago

SnarkBoojum commented 2 years ago

I'm having a hard time compiling the last version: I use "make" for the purpose, but since this compilation target also tries to do installation (which it shouldn't), it fails because it lacks the permission.

SnarkBoojum commented 2 years ago

If I try "DESTDIR=debian/tmp make", then the compilation fails because apparently at some point a compilation step needs a previous one to actually be installed and found by ocamlfind to succeed.

SnarkBoojum commented 2 years ago

I think I managed to build things, but I needed to export DESTDIR, OCAMLPATH and COQPATH, so things are a bit... hackish.

lukaszcz commented 2 years ago

"make" just does "make tactics", "make install-tactics" and then "make plugin".

The problem is that the tactics need to be installed for plugin compilation. I had a different build process with "make" which compiled everything without installing the tactics, but it broke after Coq PR https://github.com/coq/coq/pull/15220 and I don't know how to fix it, so I removed it.