coq-community/coq-dpdgraph

make install fails: no setting for BINDIR

jonleivent opened this issue · 5 comments

I tried building from a git clone, but make install failed because the env var BINDIR is not set. What were you expecting BINDIR to be set to? Would any dir for binaries on PATH work (say ~/bin, if I have that on PATH)?

This makes me discover that I never use "make install" when compiling directly from the git clone.

A priori, you should just set BINDIR to whatever directory you want the two programs dpd2dot and dpdusage to be copied to. I will check.

Apparently, I did not follow the usual practice when designing the install phase. In the opam files, the install directive is

make install BINDIR=

Choosing a directory that is in your path is sensible. I will redesign both coq-dpdgraph and the opam
description to make sure the BINDIR variable is set at configure time.

OK - thanks. I would rather not do make install if I don't have to - and just leave things in their own git repo clone. Maybe the README directions should say that "make install" is optional or something to that effect.

Actually, make install makes the plugin more handy to use, so the README directions should still suggest it as the preferred choice, I believe. There are several plugin and *.vo files that should rather be incorporated in the Coq library than left in the current directory. At the same time, it is relevant to make so that the dpd2dot and dpdusage files are copied to the directory where coqc is found.

I fixed the configure and Makefile templates so that make install will both place the vo and plugin files inside the coq installation and the binary files at the same place where coqc was found.