The Coq mailing list

[Andrew Harris <andrew.unit AT gmail.com>]

Hello,

   So I solved my problem.  It turns out that I had installed the haskell platform from a tarball and it had, for some reason, linked /usr/local/share/man/man1 to /usr/local/haskell/ghc-7.8.3-x86_64/share/man/man1/ghc.1 -- which doesn't make any sense to me.  In any case once I removed that link the coq make install step worked fine and then I just added a link inside the new man1 directory to the ghc.1 man page and everything looks good now.  Thanks again Matej for the suggestion.

-andrew

On Sun, Apr 12, 2015 at 4:29 PM, Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> wrote:

On 11/04/15 22:39, Andrew Harris wrote:
> Hello,  I'm trying to install coq8.5beta from source.  I can do the ./configure and make world steps OK.  But when I get to the make install step, I'm getting an error during the install:

Hi,

I am using Debian stable.
I had problems *building* Coq before.
After some experiments, I found that this sequence of commands works for me reliably:

  git pull  # if necessary
  make archclean && ./configure -annotate -prefix /usr/local && make clean && make world && make install

The devil is hidden in "make archclean".
I do not think that it is supposed to be a necessary step, but if I omitted it, rebuilding of Coq was failing.

>
> install -d "/usr/local/lib/coq"/plugins/micromega
> install plugins/micromega/csdpcert "/usr/local/lib/coq"/plugins/micromega
> rm -f "/usr/local/lib/coq"/revision
> install -m 644  revision "/usr/local/lib/coq"
> install: cannot stat `revision': No such file or directory
> make[1]: [install-library] Error 1 (ignored)
> install -d "/usr/local/share/man"/man1
> install: cannot create directory `/usr/local/share/man/man1': File exists
> make[1]: *** [install-coq-manpages] Error 1
> make[1]: Leaving directory `/home/andrewha/Downloads/coq-8.5beta1'
> make: *** [submake] Error 2
>
> Any help would be appreciated.
>
> -andrew